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.
pydddhttps://github.com/fpom/pyddd (Python binding for libDDD)pytlhttps://github.com/fpom/pytl (Python parser and translator for varied temporal logics)
The symbolic representation of the model must be :
- a sdd for the state space (see pyddd)
- a shom (for CTL) or a dict linking list of label strings to shoms (for (F)ARCTL) for the precedence relation (see pyddd)
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 or by a pytl.Phi object).
The method check returns the sdd representing the states that satisfy the formula.
Example :
from pymc import CTL_model_checker, FARCTL_model_checker
%run -m ecco Borana_model_ARCTL.rr
G = model(compact=False, split=False)
CTL_mc = CTL_model_checker(G.lts.states, G.lts.pred)
formula_CTL = 'EG(Gr)'
print(G.lts.init<=CTL_mc.check(formula_CTL))
actions = dict()
for rule in G.model.spec.rules:
rname = rule.name()
if G.model.spec.labels.get(rname):
labels = [l.strip() for l in G.model.spec.labels[rname].split(",")]
else:
labels = []
labels.append(rname)
actions[G.lts.tpred[rname]] = labels
FARCTL_mc = FARCTL_model_checker(G.lts.states, actions)
formula_FARCTL = '{~("Fb-" | "Wl+")}[WFAIR {"Ig+"}]AF(~Gr)'
print(G.lts.init<=FARCTL_mc.check(formula_FARCTL))
The syntax of FARCTL formula is defined by pytl :
phi ::= "(" phi ")"
| "~" phi
| quantifier phi
| unarymod phi
| phi boolop phi
| phi binarymod phi
| atom
quantifier ::= ("A" | "E") ("{" actions "}")?
unarymod ::= ("X" | "F" | "G") ("{" actions "}")?
boolop ::= "&" | "|" | "=>" | "<=>"
binarymod ::= ("{" actions "}")? ("U" | "R" | "W" | "M") ("{" actions "}")?
atom ::= /\w+|"[^\"]+"|'[^\']+'/
actions ::= "(" actions ")"
| "~" actions
| actions boolop actions
| atom