jeltz/heptagon
1
0
Fork 0
Code Issues Pull requests Releases Activity

Added initialization bad tests and correct good/t1

Browse source
This commit is contained in:
Léonard Gérard 2010-10-08 14:43:59 +02:00 committed by Léonard Gérard
parent 9414fdc5a8
commit bdcdbddb09
4 changed files with 31 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
test/bad/t10-initialization.ept Normal file
View file

@ -0,0 +1,12 @@
node toto() returns (o : int)
var last x : int; y,z : int;
let
y = 0;
automaton
state S1
do x = pre y; z = 0 -> x until true then S2
state S2
do x = last x; z = x until false then S1
end;
o = z;
tel

11
test/bad/t11-initialization.ept Normal file
View file

@ -0,0 +1,11 @@
node mmm(x: int) returns (o': int)
var last m: int; o: int;
let
automaton
state I
do m = 1; o = last m + 2 until (o = 1) then J
state J
do m = last m + 1; o = 0
end;
o' = 1 -> pre o
tel

6
test/bad/t9-initialization.ept Normal file
View file

@ -0,0 +1,6 @@
node toto() returns (o : int)
var last x : int;
let
o = x;
x = last x;
tel

4
test/good/t1.ept
View file

@ -18,11 +18,11 @@ node mm(x: int) returns (o: int)
tel
node mmm(x: int) returns (o': int)
var last m: int; o: int;
var last m: int = 1; o: int;
let
automaton
state I
do m = 1; o = last m + 2 until (o = 1) then J
do m = 0; o = last m + 1 until (o = 1) then J
state J
do m = last m + 1; o = 0
end;