Author: niels
Date: Mon May 26 13:40:14 2014
New Revision: 9454
URL: http://svn.gna.org/viewcvs/service-tech?rev=9454&view=rev
Log:
* re-introduced shortcut operators IMPOSSIBLE, INVARIANT, and REACHABLE (for
the MCC 2014)
Modified:
trunk/lola2/src/Frontend/Parser/LexicFormula.ll
trunk/lola2/src/Frontend/Parser/ParserFormula.yy
trunk/lola2/tests/testsuite.at
Modified: trunk/lola2/src/Frontend/Parser/LexicFormula.ll
URL:
http://svn.gna.org/viewcvs/service-tech/trunk/lola2/src/Frontend/Parser/LexicFormula.ll?rev=9454&r1=9453&r2=9454&view=diff
==============================================================================
--- trunk/lola2/src/Frontend/Parser/LexicFormula.ll (original)
+++ trunk/lola2/src/Frontend/Parser/LexicFormula.ll Mon May 26 13:40:14 2014
@@ -75,6 +75,10 @@
NEXTSTATE { return _NEXTSTATE_; }
RELEASE { return _RELEASE_; }
+REACHABLE { return _REACHABLE_; }
+INVARIANT { return _INVARIANT_; }
+IMPOSSIBLE { return _IMPOSSIBLE_; }
+
[AGEFXUR]+ { ptformula_lval.yt_casestring =
kc::mkcasestring(ptformula_text); return _CTLOPERATOR_; }
\; { return _semicolon_; }
Modified: trunk/lola2/src/Frontend/Parser/ParserFormula.yy
URL:
http://svn.gna.org/viewcvs/service-tech/trunk/lola2/src/Frontend/Parser/ParserFormula.yy?rev=9454&r1=9453&r2=9454&view=diff
==============================================================================
--- trunk/lola2/src/Frontend/Parser/ParserFormula.yy (original)
+++ trunk/lola2/src/Frontend/Parser/ParserFormula.yy Mon May 26 13:40:14 2014
@@ -63,6 +63,9 @@
%token _EVENTUALLY_ "temporal operator EVENTUALLY"
%token _EXPATH_ "path quantifier EXPATH"
%token _UNTIL_ "temporal operator UNTIL"
+%token _REACHABLE_ "keyword REACHABLE"
+%token _INVARIANT_ "keyword INVARIANT"
+%token _IMPOSSIBLE_ "keyword IMPOSSIBLE"
%token _notequal_ "not-equals sign"
%token _implies_ "Boolean implication"
%token _equals_ "equals sign"
@@ -183,6 +186,12 @@
}
| _NEXTSTATE_ statepredicate
{ $$ = NextState($2); }
+| _REACHABLE_ statepredicate
+ { $$ = ExPath(Eventually($2)); }
+| _INVARIANT_ statepredicate
+ { $$ = AllPath(Always($2)); }
+| _IMPOSSIBLE_ statepredicate
+ { $$ = AllPath(Always(Negation($2))); }
;
atomic_proposition:
Modified: trunk/lola2/tests/testsuite.at
URL:
http://svn.gna.org/viewcvs/service-tech/trunk/lola2/tests/testsuite.at?rev=9454&r1=9453&r2=9454&view=diff
==============================================================================
--- trunk/lola2/tests/testsuite.at (original)
+++ trunk/lola2/tests/testsuite.at Mon May 26 13:40:14 2014
@@ -1208,6 +1208,27 @@
AT_SETUP([Temporal operators: EXPATH EVENTUALLY])
AT_CHECK([cp TESTFILES/garavel.lola .])
AT_CHECK([LOLA garavel.lola --check=none --formula='"FORMULA EXPATH EVENTUALLY
p.1 <= 1;"'],0,stdout,stderr)
+AT_CHECK([GREP -q "lola: processed formula with 1 atomic propositions" stderr])
+AT_KEYWORDS(formula)
+AT_CLEANUP
+
+AT_SETUP([Temporal operators: REACHABLE])
+AT_CHECK([cp TESTFILES/garavel.lola .])
+AT_CHECK([LOLA garavel.lola --check=none --formula='"FORMULA REACHABLE p.1 <=
1;"'],0,stdout,stderr)
+AT_CHECK([GREP -q "lola: processed formula with 1 atomic propositions" stderr])
+AT_KEYWORDS(formula)
+AT_CLEANUP
+
+AT_SETUP([Temporal operators: INVARIANT])
+AT_CHECK([cp TESTFILES/garavel.lola .])
+AT_CHECK([LOLA garavel.lola --check=none --formula='"FORMULA INVARIANT p.1 <=
1;"'],0,stdout,stderr)
+AT_CHECK([GREP -q "lola: processed formula with 1 atomic propositions" stderr])
+AT_KEYWORDS(formula)
+AT_CLEANUP
+
+AT_SETUP([Temporal operators: IMPOSSIBLE])
+AT_CHECK([cp TESTFILES/garavel.lola .])
+AT_CHECK([LOLA garavel.lola --check=none --formula='"FORMULA IMPOSSIBLE p.1 <=
1;"'],0,stdout,stderr)
AT_CHECK([GREP -q "lola: processed formula with 1 atomic propositions" stderr])
AT_KEYWORDS(formula)
AT_CLEANUP
--
You received this e-mail, because you subscribed the mailing list
"service-tech-commits" which will forward you any e-mail addressed to
[email protected]. If you want to unsubscribe or make any changes to
your subscription, please go to
https://mail.gna.org/listinfo/service-tech-commits.
