Closed mgieseking closed 4 years ago
Ok, I have made a "help" modal with shortcuts and a place to put the MC syntax. Can you provide me with an appropriate text to show the mc syntax? (HTML would be great)
The header should be Flow-LTL syntax.
The syntax for Flow-LTL is given by:
phi = LTL | ( phi AND phi ) | ( phi OR phi ) | ( LTL -> phi ) | A LTL
with standard LTL formulas with the following operators:
LTL | Syntax |
---|---|
true | TRUE |
false | FALSE |
atoms | place and transition ids |
Negation | NEG or ! |
Next | X |
Conjunction | AND |
Disjunction | OR |
Implication | IMP or -> |
Bimplication | BIMP or <-> |
Until | U |
Weak Until | W |
Release | R |
Binary operators have to be in brackets, unary operators not. For example (!phi0 -> (phi1 AND G F phi2)). Note that the ids for the places and transitions are more restricted for the formula as for the web interface.
Nice, thanks :)
I put the formula syntax and a link to the github documentation in there. Can you check it out and close the issue if this works for you?
The user guide link takes you to the one corresponding to the mode you are in (mc or synt).
Currently I don't see the user guide in the synt case? But otherwise everything is good.
Ah, thanks :) I have unhidden it in 4b7f4d78faed786f3146b72638f3f9999cc0de2a
In the menu bar add a help item (see #75) with