Toggle navigation
Toggle navigation
This project
Loading...
Sign in
Colin THOMAS
/
pyits_model_checker
Go to a project
Toggle navigation
Toggle navigation pinning
Projects
Groups
Snippets
Help
Project
Activity
Repository
Pipelines
Graphs
Issues
0
Merge Requests
0
Wiki
Network
Create a new issue
Builds
Commits
Authored by
Colin THOMAS
2020-12-11 08:50:23 +0000
Browse Files
Options
Browse Files
Download
Email Patches
Plain Diff
Commit
53f5c9582b2220797e6b7d7b69008d2630c80e82
53f5c958
1 parent
a9779046
Update README.md
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
36 additions
and
6 deletions
README.md
README.md
View file @
53f5c95
...
...
@@ -41,9 +41,15 @@ The syntax of formulae is described at [pytl](https://github.com/fpom/pytl) :
| "(" phi ")"
| atom
Supported operators :
-
unary :
`EX, EF, EG, AX, AF, AG`
-
binary :
`EU, EW, ER, AU, AW, AR`
quantifier ::= "A" | "E"
unarymod ::= "X" | "F" | "G"
boolop ::= "&" | "|" | "=>" | "<=>"
binarymod ::= "U" | "R"
atom ::= /\w+|"[^"]+"|'[^']+'/
### Fair CTL
...
...
@@ -54,6 +60,30 @@ An additional argument must be given at initialization, representing the fairnes
-
a list of strings, Phi objects or sdd, representing the list of fairness constraints :
[
f1, f2,...
]
-
a single string, Phi or sdd, representing a single fairness constraint
Supported operators :
-
unary :
`EX, EF, EG, AX, AF, AG`
-
binary :
`EU, AU`
### ARCTL
The syntax of formulae is described at
[
pytl
](
https://github.com/fpom/pytl
)
:
phi ::= quantifier unarymod phi
| quantifier phi binarymod phi
| phi boolop phi
| "~" phi
| "(" phi ")"
| atom
quantifier ::= ("A" | "E") ("{" actions "}")?
unarymod ::= "X" | "F" | "G"
boolop ::= "&" | "|" | "=>" | "<=>"
binarymod ::= "U" | "R"
atom ::= /\w+|"[^"]+"|'[^']+'/
actions ::= "(" actions ")"
| "~" actions
| actions boolop actions
| atom
### FairARCTL
...
...
Please
register
or
login
to post a comment