alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

tut03: add missing operators

Browse source 
* doc/org/tut03.org: Here.
This commit is contained in:
Alexandre Duret-Lutz 2019-05-06 15:15:44 +02:00
parent 6fac026454
commit ef8de879dc
1 changed files with 8 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

8
doc/org/tut03.org
View file

@ -41,10 +41,14 @@ Here is the list of supported operators:
// unary operators // unary operators
formula::Not(arg); formula::Not(arg);
formula::X(arg); formula::X(arg);
formula::X(arg, min, max); // X[min..max] arg
formula::F(arg); formula::F(arg);
formula::F(arg, min, max); // F[min..max] arg
formula::G(arg); formula::G(arg);
formula::G(arg, min, max); // G[min..max] arg
formula::Closure(arg); formula::Closure(arg);
formula::NegClosure(arg); formula::NegClosure(arg);
formula::first_match(arg); // SVA's first match opetaror
// binary operators // binary operators
formula::Xor(left, right); formula::Xor(left, right);
formula::Implies(left, right); formula::Implies(left, right);
@ -66,6 +70,10 @@ Here is the list of supported operators:
// star-like operators // star-like operators
formula::Star(arg, min, max); // Star (for a Kleene star, set min=0 and omit max) formula::Star(arg, min, max); // Star (for a Kleene star, set min=0 and omit max)
formula::FStar(arg, min, max); // Fusion Star formula::FStar(arg, min, max); // Fusion Star
// syntactic sugar built on top of previous operators
formula::sugar_goto(arg, min, max); // arg[->min..max]
formula::sugar_equal(arg, min, max); // arg[=min..max]
formula::sugar_delay(left, right, min, max); // left ##[min..max] right
#+END_SRC #+END_SRC
These functions implement some very limited type of automatic These functions implement some very limited type of automatic