diff --git a/src/plugins/aorai/tests/ya/metavariables-incompatible.ya b/src/plugins/aorai/tests/ya/metavariables-incompatible.ya
index 059f0d555ba7fa97e2d82f9988a895f06b968132..1a112501655fc5b2f4a9a0b3ed80cb9aacce7288 100644
--- a/src/plugins/aorai/tests/ya/metavariables-incompatible.ya
+++ b/src/plugins/aorai/tests/ya/metavariables-incompatible.ya
@@ -4,6 +4,6 @@
$x : int;
-a : { CALL(main)* } -> b;
+a : { [CALL(main)]* } -> b;
b : -> b;
diff --git a/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle
index 924f3f034437969ed4962e44e7adc894e8367e12..009f14f70dd4771f190e1b6b609515a3a8316b8a 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle
@@ -72,11 +72,11 @@ enum aorai_OpStatusList {
ensures 0 ≡ S1;
behavior buch_state_S2_in:
- assumes 1 ≡ S1 ∧ 1 ≢ 0;
+ assumes 1 ≡ S1;
ensures 1 ≡ S2;
behavior buch_state_S2_out:
- assumes 0 ≡ S1 ∨ 1 ≡ 0;
+ assumes 0 ≡ S1;
ensures 0 ≡ S2;
behavior buch_state_main_0_out:
@@ -106,7 +106,6 @@ enum aorai_OpStatusList {
/*@ requires 1 ≡ S1 ∧ 0 ≡ S2 ∧ 0 ≡ main_0;
behavior Buchi_property_behavior:
- ensures 1 ≡ S2 ⇒ 1 ≢ 0;
ensures 1 ≡ S1 ∨ 0 ≡ S1;
ensures 1 ≡ S2 ∨ 0 ≡ S2;
ensures 0 ≡ main_0;
@@ -186,7 +185,6 @@ int decode_int(char *s)
/*@ ghost
/@ requires (1 ≡ S1 ∨ 1 ≡ S2) ∧ 0 ≡ main_0;
- requires 1 ≡ S1 ⇒ 1 ≢ 0;
ensures aorai_CurOpStatus ≡ aorai_Called;
ensures aorai_CurOperation ≡ op_factorial;
assigns aorai_CurOpStatus, aorai_CurOperation, S1, S2, main_0;
@@ -195,11 +193,11 @@ int decode_int(char *s)
ensures 0 ≡ S1;
behavior buch_state_S2_in:
- assumes 1 ≡ S2 ∨ (1 ≡ S1 ∧ 1 ≢ 0);
+ assumes 1 ≡ S2 ∨ 1 ≡ S1;
ensures 1 ≡ S2;
behavior buch_state_S2_out:
- assumes 0 ≡ S2 ∧ (0 ≡ S1 ∨ 1 ≡ 0);
+ assumes 0 ≡ S2 ∧ 0 ≡ S1;
ensures 0 ≡ S2;
behavior buch_state_main_0_out:
@@ -241,11 +239,11 @@ int decode_int(char *s)
ensures 0 ≡ S1;
behavior buch_state_S2_in:
- assumes 1 ≡ S2 ∨ (1 ≡ S1 ∧ 1 ≢ 0);
+ assumes 1 ≡ S2 ∨ 1 ≡ S1;
ensures 1 ≡ S2;
behavior buch_state_S2_out:
- assumes 0 ≡ S2 ∧ (0 ≡ S1 ∨ 1 ≡ 0);
+ assumes 0 ≡ S2 ∧ 0 ≡ S1;
ensures 0 ≡ S2;
behavior buch_state_main_0_out:
@@ -273,7 +271,6 @@ int decode_int(char *s)
*/
/*@ requires (1 ≡ S1 ∨ 1 ≡ S2) ∧ 0 ≡ main_0;
- requires 1 ≡ S1 ⇒ 1 ≢ 0;
requires 1 ≡ S2 ∨ 0 ≡ S2;
requires 1 ≡ S1 ∨ 0 ≡ S1;
requires 0 ≤ value ≤ 12;
@@ -356,11 +353,11 @@ int factorial(int value)
ensures 0 ≡ S1;
behavior buch_state_S2_in:
- assumes 1 ≡ S1 ∧ 1 ≢ 0;
+ assumes 1 ≡ S1;
ensures 1 ≡ S2;
behavior buch_state_S2_out:
- assumes 0 ≡ S1 ∨ 1 ≡ 0;
+ assumes 0 ≡ S1;
ensures 0 ≡ S2;
behavior buch_state_main_0_out:
@@ -392,7 +389,6 @@ int factorial(int value)
ensures \result ≡ 0 ∨ \result ≡ 1;
behavior Buchi_property_behavior:
- ensures 1 ≡ S2 ⇒ 1 ≢ 0;
ensures 1 ≡ S1 ∨ 0 ≡ S1;
ensures 1 ≡ S2 ∨ 0 ≡ S2;
ensures 0 ≡ main_0;
diff --git a/src/plugins/aorai/tests/ya/test_factorial.ya b/src/plugins/aorai/tests/ya/test_factorial.ya
index 40b7d74fdf4ec3848c29201687a4af06a7169ad9..5591fef945d20e12264d77820ad2616fbca7ffc8 100644
--- a/src/plugins/aorai/tests/ya/test_factorial.ya
+++ b/src/plugins/aorai/tests/ya/test_factorial.ya
@@ -5,7 +5,7 @@ main : { !CALL(factorial) } -> S1
| -> S2
;
S1 : { !CALL(factorial) } -> S1
- | { 1 } -> S2
+ | { true } -> S2
;
S2 : {!CALL(factorial) && COR(factorial) } -> S1
| { COR(factorial) } -> S2
diff --git a/src/plugins/aorai/yaparser.mly b/src/plugins/aorai/yaparser.mly
index 1b0b7c2ae0e42429eaa7aa1bc62772740240ab4a..5ea7debd775d65becc5372bc921f814181a3e3ec 100644
--- a/src/plugins/aorai/yaparser.mly
+++ b/src/plugins/aorai/yaparser.mly
@@ -148,8 +148,6 @@ type pre_cond = Behavior of string | Pre of Promelaast.condition
%token OTHERWISE
%token EOF
-%left OR AND
-%nonassoc NOT
%left STAR
%left DOT
%left LSQUARE
@@ -254,7 +252,6 @@ seq:
;
guard:
- | single_cond { to_seq $1 }
| LSQUARE non_empty_seq RSQUARE { $2 }
| IDENTIFIER pre_cond LPAREN seq RPAREN post_cond
{ let pre_cond =
@@ -289,15 +286,16 @@ guard:
pre_cond:
| COLUMNCOLUMN IDENTIFIER { Behavior $2 }
- | LBRACELBRACE single_cond RBRACERBRACE { Pre $2 }
+ | LBRACELBRACE cond RBRACERBRACE { Pre $2 }
;
post_cond:
| /* epsilon */ { None }
- | LBRACELBRACE single_cond RBRACERBRACE { Some $2 }
+ | LBRACELBRACE cond RBRACERBRACE { Some $2 }
;
seq_elt:
+ | cond { to_seq $1 }
| guard repetition {
let min, max = $2 in
match $1 with
@@ -321,17 +319,23 @@ repetition:
| LCURLY arith_relation COMMA RCURLY { Some $2, None }
| LCURLY COMMA arith_relation RCURLY { None, Some $3 }
-single_cond:
+cond:
+ | conjunction OR cond { POr ($1,$3) }
+ | conjunction { $1 }
+
+conjunction:
+ | atomic_cond AND conjunction { PAnd($1,$3) }
+ | atomic_cond { $1 }
+
+atomic_cond:
| CALLORRETURN_OF LPAREN IDENTIFIER RPAREN
{ POr (PCall ($3,None), PReturn $3) }
| CALL_OF LPAREN IDENTIFIER RPAREN { PCall ($3,None) }
| RETURN_OF LPAREN IDENTIFIER RPAREN { PReturn $3 }
| TRUE { PTrue }
| FALSE { PFalse }
- | NOT single_cond { PNot $2 }
- | single_cond AND single_cond { PAnd ($1,$3) }
- | single_cond OR single_cond { POr ($1,$3) }
- | LPAREN single_cond RPAREN { $2 }
+ | NOT atomic_cond { PNot $2 }
+ | LPAREN cond RPAREN { $2 }
| logic_relation { $1 }
;
@@ -342,7 +346,7 @@ logic_relation
| arith_relation LE arith_relation { PRel(Le, $1, $3) }
| arith_relation GE arith_relation { PRel(Ge, $1, $3) }
| arith_relation NEQ arith_relation { PRel(Neq, $1, $3) }
- | arith_relation { PRel (Neq, $1, PCst(IntConstant "0")) }
+/* | arith_relation { PRel (Neq, $1, PCst(IntConstant "0")) } */
;
arith_relation
@@ -352,9 +356,9 @@ arith_relation
;
arith_relation_mul
- : arith_relation_mul SLASH access_or_const { PBinop(Bdiv,$1,$3) }
- | arith_relation_mul STAR access_or_const { PBinop(Bmul, $1, $3) }
- | arith_relation_mul PERCENT access_or_const { PBinop(Bmod, $1, $3) }
+ : arith_relation_mul SLASH arith_relation_bw { PBinop(Bdiv,$1,$3) }
+ | arith_relation_mul STAR arith_relation_bw { PBinop(Bmul, $1, $3) }
+ | arith_relation_mul PERCENT arith_relation_bw { PBinop(Bmod, $1, $3) }
| arith_relation_bw { $1 }
;
@@ -382,7 +386,7 @@ access_leaf
: STAR access { PUnop (Ustar,$2) }
| IDENTIFIER LPAREN RPAREN DOT IDENTIFIER { PPrm($1,$5) }
| IDENTIFIER { PVar $1 }
- | LPAREN access RPAREN { $2 }
+ | LPAREN arith_relation RPAREN { $2 }
| METAVAR { PMetavar $1 }
;