Showing
1 changed file
with
18 additions
and
14 deletions
| ... | @@ -217,12 +217,12 @@ def build_labeled_succ(v): | ... | @@ -217,12 +217,12 @@ def build_labeled_succ(v): |
| 217 | 217 | ||
| 218 | 218 | ||
| 219 | class ARCTL_model_checker(CTL_model_checker): | 219 | class ARCTL_model_checker(CTL_model_checker): |
| 220 | - def __init__ (self, universe, succ_dict, true_label="_None"): | 220 | + def __init__ (self, universe, succ_dict, tau_label="_None"): |
| 221 | """ | 221 | """ |
| 222 | Input : | 222 | Input : |
| 223 | - universe is a sdd representing the state space (for example v.g.reachable) | 223 | - universe is a sdd representing the state space (for example v.g.reachable) |
| 224 | - succ_dict is a dictionary associating transition label strings to shom representing the succ for this label (for exemple using build_dict_labeled_succ(v)) | 224 | - succ_dict is a dictionary associating transition label strings to shom representing the succ for this label (for exemple using build_dict_labeled_succ(v)) |
| 225 | - - true_label : the label representing invisible actions, or False if no invisible actions | 225 | + - tau_label : the label representing invisible actions, or None if no invisible actions |
| 226 | """ | 226 | """ |
| 227 | assert isinstance(succ_dict, dict), "succ_dict must be of type dict" | 227 | assert isinstance(succ_dict, dict), "succ_dict must be of type dict" |
| 228 | assert len(succ_dict) >= 1, "succ_dict must contain at least one element" | 228 | assert len(succ_dict) >= 1, "succ_dict must contain at least one element" |
| ... | @@ -230,14 +230,15 @@ class ARCTL_model_checker(CTL_model_checker): | ... | @@ -230,14 +230,15 @@ class ARCTL_model_checker(CTL_model_checker): |
| 230 | assert isinstance(e, str), "every key of succ_dict must be of type string" | 230 | assert isinstance(e, str), "every key of succ_dict must be of type string" |
| 231 | assert isinstance(succ_dict[e], shom), "every value of succ_dict must be of type shom" | 231 | assert isinstance(succ_dict[e], shom), "every value of succ_dict must be of type shom" |
| 232 | 232 | ||
| 233 | - | ||
| 234 | self.succ_dict = succ_dict | 233 | self.succ_dict = succ_dict |
| 235 | - self.true_label = true_label | 234 | + if tau_label in succ_dict: |
| 235 | + self.tau_label = tau_label | ||
| 236 | + else: | ||
| 237 | + self.tau_label = None | ||
| 236 | self.succ = functools.reduce(shom.__or__, self.succ_dict.values(), shom.empty()) | 238 | self.succ = functools.reduce(shom.__or__, self.succ_dict.values(), shom.empty()) |
| 237 | CTL_model_checker.__init__(self, universe, self.succ) | 239 | CTL_model_checker.__init__(self, universe, self.succ) |
| 238 | self.logic = "ARCTL" | 240 | self.logic = "ARCTL" |
| 239 | 241 | ||
| 240 | - | ||
| 241 | def build_succ_alpha(self, alpha): | 242 | def build_succ_alpha(self, alpha): |
| 242 | if alpha.kind == 'bool': | 243 | if alpha.kind == 'bool': |
| 243 | assert isinstance(alpha.value, bool), repr(alpha) + " is of kind bool but its value is not a boolean" | 244 | assert isinstance(alpha.value, bool), repr(alpha) + " is of kind bool but its value is not a boolean" |
| ... | @@ -272,16 +273,15 @@ class ARCTL_model_checker(CTL_model_checker): | ... | @@ -272,16 +273,15 @@ class ARCTL_model_checker(CTL_model_checker): |
| 272 | # recursive function that builds the sdd along the syntax tree (bottom-up, going-up from the tree leaves) | 273 | # recursive function that builds the sdd along the syntax tree (bottom-up, going-up from the tree leaves) |
| 273 | def _phi2sdd(self, phi): | 274 | def _phi2sdd(self, phi): |
| 274 | if phi.actions: | 275 | if phi.actions: |
| 276 | + succ = self.build_succ_alpha(phi.actions) | ||
| 277 | + if self.tau_label: | ||
| 278 | + succ = shom.__or__(succ, self.succ_dict[self.tau_label])# the invisible actions are added to succ | ||
| 275 | if phi.kind in self.unarymod: | 279 | if phi.kind in self.unarymod: |
| 276 | - succ = self.build_succ_alpha(phi.actions) | ||
| 277 | - if self.true_label: | ||
| 278 | - # the invisible actions are added to succ | ||
| 279 | - succ = shom.__or__(succ, self.succ_dict["_None"]) | ||
| 280 | return CTL_model_checker(self.CTL_True, succ).unarymod[phi.kind](self._phi2sdd(phi.children[0])) | 280 | return CTL_model_checker(self.CTL_True, succ).unarymod[phi.kind](self._phi2sdd(phi.children[0])) |
| 281 | elif phi.kind in self.binarymod: | 281 | elif phi.kind in self.binarymod: |
| 282 | return CTL_model_checker(self.CTL_True, succ).binarymod[phi.kind](self._phi2sdd(phi.children[0]), self._phi2sdd(phi.children[1])) | 282 | return CTL_model_checker(self.CTL_True, succ).binarymod[phi.kind](self._phi2sdd(phi.children[0]), self._phi2sdd(phi.children[1])) |
| 283 | else: | 283 | else: |
| 284 | - return CTL_model_checker._phi2sdd(phi) | 284 | + return CTL_model_checker._phi2sdd(self, phi) |
| 285 | 285 | ||
| 286 | 286 | ||
| 287 | 287 | ||
| ... | @@ -294,9 +294,13 @@ class FairARCTL_model_checker(ARCTL_model_checker, FairCTL_model_checker): | ... | @@ -294,9 +294,13 @@ class FairARCTL_model_checker(ARCTL_model_checker, FairCTL_model_checker): |
| 294 | 294 | ||
| 295 | # recursive function that builds the sdd along the syntax tree (bottom-up, going-up from the tree leaves) | 295 | # recursive function that builds the sdd along the syntax tree (bottom-up, going-up from the tree leaves) |
| 296 | def _phi2sdd(self, phi): | 296 | def _phi2sdd(self, phi): |
| 297 | - if phi.kind in self.unarymod and phi.actions: | 297 | + if phi.actions: |
| 298 | - return FairCTL_model_checker(self.CTL_True, self.build_succ_alpha(phi.actions), self.fairness).unarymod[phi.kind](self._phi2sdd(phi.children[0])) | 298 | + succ = self.build_succ_alpha(phi.actions) |
| 299 | - elif phi.kind in self.binarymod and phi.actions: | 299 | + if self.tau_label: |
| 300 | - return FairCTL_model_checker(self.CTL_True, self.build_succ_alpha(phi.actions), self.fairness).binarymod[phi.kind](self._phi2sdd(phi.children[0]), self._phi2sdd(phi.children[1])) | 300 | + succ = shom.__or__(succ, self.succ_dict[self.tau_label])# the invisible actions are added to succ |
| 301 | + if phi.kind in self.unarymod: | ||
| 302 | + FairCTL_model_checker(self.CTL_True, succ, self.fairness).unarymod[phi.kind](self._phi2sdd(phi.children[0])) | ||
| 303 | + elif phi.kind in self.binarymod: | ||
| 304 | + return FairCTL_model_checker(self.CTL_True, succ, self.fairness).binarymod[phi.kind](self._phi2sdd(phi.children[0]), self._phi2sdd(phi.children[1])) | ||
| 301 | else: | 305 | else: |
| 302 | return FairCTL_model_checker._phi2sdd(self, phi) | 306 | return FairCTL_model_checker._phi2sdd(self, phi) |
| ... | \ No newline at end of file | ... | \ No newline at end of file | ... | ... |
-
Please register or login to post a comment