Showing
1 changed file
with
14 additions
and
15 deletions
... | @@ -136,29 +136,28 @@ class CTL_model_checker(object): | ... | @@ -136,29 +136,28 @@ class CTL_model_checker(object): |
136 | 136 | ||
137 | 137 | ||
138 | class ARCTL_model_checker(CTL_model_checker): | 138 | class ARCTL_model_checker(CTL_model_checker): |
139 | - def __init__ (self, universe, pred_dict, pred, tau_label="_None"): | 139 | + def __init__ (self, universe, actions, tau_label="_None"): |
140 | """ | 140 | """ |
141 | Input: | 141 | Input: |
142 | - universe is a sdd representing the state space (for example v.g.reachable) | 142 | - universe is a sdd representing the state space (for example v.g.reachable) |
143 | - - pred_dict is a list of tuples associating shoms and vectors of label strings | 143 | + - actions is a list of tuples associating shoms and vectors of label strings |
144 | - - pred is a shom representing the precedence relation (inverse of the transition relation) | ||
145 | - tau_label is the label representing invisible actions, or '_None' if no invisible actions | 144 | - tau_label is the label representing invisible actions, or '_None' if no invisible actions |
146 | """ | 145 | """ |
147 | - assert isinstance(pred_dict, list), "pred_dict must be of type dict" | 146 | + assert isinstance(actions, list), "actions must be of type dict" |
148 | - self.pred_dict = pred_dict | 147 | + assert len(actions) >= 1, "actions must contain at least one element" |
149 | - assert len(pred_dict) >= 1, "pred_dict must contain at least one element" | 148 | + self.actions = actions |
150 | - self.alpha_labels = set() | 149 | + self.action_labels = set() |
151 | - for action, labels in pred_dict: # for each key of the dictionnary | 150 | + for action, labels in self.actions: # for each key of the dictionnary |
152 | - assert isinstance(action, shom), "every key of pred_dict must be of type shom" | 151 | + assert isinstance(action, shom), "every key of actions must be of type shom" |
153 | for l in labels: | 152 | for l in labels: |
154 | - assert isinstance(l, str), "every value of pred_dict must be of type str" | 153 | + assert isinstance(l, str), "every value of actions must be of type str" |
155 | - self.alpha_labels.add(l) | 154 | + self.action_labels.add(l) |
156 | self.alpha_labels = list(self.alpha_labels) | 155 | self.alpha_labels = list(self.alpha_labels) |
157 | - if tau_label in self.alpha_labels: | 156 | + if tau_label in self.action_labels: |
158 | self.tau_label = tau_label | 157 | self.tau_label = tau_label |
159 | else: | 158 | else: |
160 | self.tau_label = None | 159 | self.tau_label = None |
161 | - CTL_model_checker.__init__(self, universe, pred) | 160 | + CTL_model_checker.__init__(self, universe, reduce(shom.__or__, [action for (action, labels) in self.actions])) |
162 | self.logic = "ARCTL" | 161 | self.logic = "ARCTL" |
163 | 162 | ||
164 | def alpha_parse(self, alpha, labels): | 163 | def alpha_parse(self, alpha, labels): |
... | @@ -169,7 +168,7 @@ class ARCTL_model_checker(CTL_model_checker): | ... | @@ -169,7 +168,7 @@ class ARCTL_model_checker(CTL_model_checker): |
169 | else: | 168 | else: |
170 | return False | 169 | return False |
171 | elif alpha.kind == 'name': | 170 | elif alpha.kind == 'name': |
172 | - assert alpha.value in self.alpha_labels, f"{alpha.value} is not an action label" | 171 | + assert alpha.value in self.action_labels, f"{alpha.value} is not an action label" |
173 | if self.tau_label: | 172 | if self.tau_label: |
174 | if self.tau_label in labels: | 173 | if self.tau_label in labels: |
175 | return True | 174 | return True |
... | @@ -184,7 +183,7 @@ class ARCTL_model_checker(CTL_model_checker): | ... | @@ -184,7 +183,7 @@ class ARCTL_model_checker(CTL_model_checker): |
184 | raise ValueError(repr(alpha) + "is not an action sub formula") | 183 | raise ValueError(repr(alpha) + "is not an action sub formula") |
185 | 184 | ||
186 | def build_pred_alpha(self, alpha): | 185 | def build_pred_alpha(self, alpha): |
187 | - return reduce(shom.__or__, [action for (action, labels) in self.pred_dict if self.alpha_parse(alpha, labels)], shom.empty()) | 186 | + return reduce(shom.__or__, [action for (action, labels) in self.actions if self.alpha_parse(alpha, labels)], shom.empty()) |
188 | 187 | ||
189 | def check(self, formula): | 188 | def check(self, formula): |
190 | """ | 189 | """ | ... | ... |
-
Please register or login to post a comment