Showing
1 changed file
with
33 additions
and
53 deletions
1 | -# Python CTL model checker | 1 | +# Python FARCTL symbolic model checker |
2 | 2 | ||
3 | -Given a model (the symbolic representation of the statespace and the transition relation) build an object able to symbolically compute the set of states satistfying a formula (CTL, Fair CTL, wip : ACTL and ARCTL). | 3 | +Given a model (the symbolic representation of the statespace and the transition relation) build an object able to symbolically compute the set of states satistfying an (FAR)CTL formula. |
4 | 4 | ||
5 | ## Requirement | 5 | ## Requirement |
6 | - - `pyddd` [https://github.com/fpom/pyddd](https://github.com/fpom/pyddd) | 6 | + - `pyddd` [https://github.com/fpom/pyddd](https://github.com/fpom/pyddd) (Python binding for libDDD) |
7 | - - `pytl` [https://github.com/fpom/pytl](https://github.com/fpom/pytl) | 7 | + - `pytl` [https://github.com/fpom/pytl](https://github.com/fpom/pytl) (Python parser and translator for varied temporal logics) |
8 | 8 | ||
9 | ## Usage | 9 | ## Usage |
10 | 10 | ||
11 | The symbolic representation of the model must be : | 11 | The symbolic representation of the model must be : |
12 | - a sdd for the state space (see [pyddd](https://github.com/fpom/pyddd)) | 12 | - a sdd for the state space (see [pyddd](https://github.com/fpom/pyddd)) |
13 | - - a shom for the precedence relation (see [pyddd](https://github.com/fpom/pyddd)) | 13 | + - a shom (for CTL) or a dict linking list of label strings to shoms (for (F)ARCTL) for the precedence relation (see [pyddd](https://github.com/fpom/pyddd)) |
14 | 14 | ||
15 | Instantiated with such symbolic representation, the object can be called with the method check on a formula (represented by a string which will be parsed by [pytl](https://github.com/fpom/pytl) or by a `pytl.Phi` object). | 15 | Instantiated with such symbolic representation, the object can be called with the method check on a formula (represented by a string which will be parsed by [pytl](https://github.com/fpom/pytl) or by a `pytl.Phi` object). |
16 | The method `check` returns the sdd representing the states that satisfy the formula. | 16 | The method `check` returns the sdd representing the states that satisfy the formula. |
... | @@ -18,72 +18,52 @@ The method `check` returns the sdd representing the states that satisfy the form | ... | @@ -18,72 +18,52 @@ The method `check` returns the sdd representing the states that satisfy the form |
18 | 18 | ||
19 | Example : | 19 | Example : |
20 | 20 | ||
21 | - from pymc import CTL_model_checker, FairCTL_model_checker | 21 | + from pymc import CTL_model_checker, FARCTL_model_checker |
22 | - %run -m ecco termites-simpler.rr | 22 | + %run -m ecco Borana_model_ARCTL.rr |
23 | - v = model("test",split=False, force=True) | 23 | + G = model(compact=False, split=False) |
24 | - formula = "AF E(Sd U Fg & Te)" | ||
25 | - CTL_mc = CTL_model_checker(v.g.reachable, v.g.m.succ()) | ||
26 | - FairCTL_mc = FairCTL_model_checker(v.g.reachable, v.g.m.succ(),["~Ac"]) | ||
27 | - print(v.g.initial<=CTL_mc.check(formula)) | ||
28 | - print(v.g.initial<=FairCTL_mc.check(formula)) | ||
29 | 24 | ||
25 | + CTL_mc = CTL_model_checker(G.lts.states, G.lts.pred) | ||
26 | + formula_CTL = 'EG(Gr)' | ||
27 | + print(G.lts.init<=CTL_mc.check(formula_CTL)) | ||
30 | 28 | ||
31 | -### CTL | 29 | + actions = dict() |
30 | + for rule in G.model.spec.rules: | ||
31 | + rname = rule.name() | ||
32 | + if G.model.spec.labels.get(rname): | ||
33 | + labels = [l.strip() for l in G.model.spec.labels[rname].split(",")] | ||
34 | + else: | ||
35 | + labels = [] | ||
36 | + labels.append(rname) | ||
37 | + actions[G.lts.tpred[rname]] = labels | ||
38 | + FARCTL_mc = FARCTL_model_checker(G.lts.states, actions) | ||
39 | + formula_FARCTL = '{~("Fb-" | "Wl+")}[WFAIR {"Ig+"}]AF(~Gr)' | ||
40 | + print(G.lts.init<=FARCTL_mc.check(formula_FARCTL)) | ||
32 | 41 | ||
33 | -Implement the algorithm of Symbolic Model Checking, McMillan 1993, section 2.4. | ||
34 | 42 | ||
35 | -The syntax of formulae is described at [pytl](https://github.com/fpom/pytl) : | 43 | +### FARCTL |
36 | 44 | ||
37 | - phi ::= quantifier unarymod phi | 45 | +The syntax of FARCTL formula is defined by [pytl](https://github.com/fpom/pytl) : |
38 | - | quantifier phi binarymod phi | ||
39 | - | phi boolop phi | ||
40 | - | "~" phi | ||
41 | - | "(" phi ")" | ||
42 | - | atom | ||
43 | - | ||
44 | - quantifier ::= "A" | "E" | ||
45 | - | ||
46 | - unarymod ::= "X" | "F" | "G" | ||
47 | - | ||
48 | - boolop ::= "&" | "|" | "=>" | "<=>" | ||
49 | - | ||
50 | - binarymod ::= "U" | "R" | ||
51 | 46 | ||
52 | - atom ::= /\w+|"[^"]+"|'[^']+'/ | 47 | + phi ::= "(" phi ")" |
53 | - | ||
54 | -### Fair CTL | ||
55 | - | ||
56 | -Implement the algorithm of Symbolic Model Checking, McMillan 1993, section 6.4 and Symbolic model checking: 1020 states and beyond, Burch et al 1992, section 6.2. | ||
57 | - | ||
58 | -The evaluation of the formula is restricter to the trajectoriers verifying fairness constraints of the form `AND([GF f for f in fairness])`. | ||
59 | -An additional argument must be given at initialization, representing the fairness constraints : | ||
60 | - - a list of strings, Phi objects or sdd, representing the list of fairness constraints : [f1, f2,...] | ||
61 | - - a single string, Phi or sdd, representing a single fairness constraint | ||
62 | - | ||
63 | -### ARCTL | ||
64 | - | ||
65 | -The syntax of formulae is described at [pytl](https://github.com/fpom/pytl) : | ||
66 | - | ||
67 | - phi ::= quantifier unarymod phi | ||
68 | - | quantifier phi binarymod phi | ||
69 | - | phi boolop phi | ||
70 | | "~" phi | 48 | | "~" phi |
71 | - | "(" phi ")" | 49 | + | quantifier phi |
50 | + | unarymod phi | ||
51 | + | phi boolop phi | ||
52 | + | phi binarymod phi | ||
72 | | atom | 53 | | atom |
73 | 54 | ||
74 | quantifier ::= ("A" | "E") ("{" actions "}")? | 55 | quantifier ::= ("A" | "E") ("{" actions "}")? |
75 | 56 | ||
76 | - unarymod ::= "X" | "F" | "G" | 57 | + unarymod ::= ("X" | "F" | "G") ("{" actions "}")? |
77 | 58 | ||
78 | boolop ::= "&" | "|" | "=>" | "<=>" | 59 | boolop ::= "&" | "|" | "=>" | "<=>" |
79 | 60 | ||
80 | - binarymod ::= "U" | "R" | 61 | + binarymod ::= ("{" actions "}")? ("U" | "R" | "W" | "M") ("{" actions "}")? |
81 | 62 | ||
82 | - atom ::= /\w+|"[^"]+"|'[^']+'/ | 63 | + atom ::= /\w+|"[^\"]+"|'[^\']+'/ |
83 | 64 | ||
84 | actions ::= "(" actions ")" | 65 | actions ::= "(" actions ")" |
85 | | "~" actions | 66 | | "~" actions |
86 | | actions boolop actions | 67 | | actions boolop actions |
87 | | atom | 68 | | atom |
88 | 69 | ||
89 | -### FairARCTL | ... | ... |
-
Please register or login to post a comment