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

Add lib/pervasives.epi, tests, tools

Browse source
This commit is contained in:
Léonard Gérard 2010-06-21 12:11:06 +02:00
parent 60a3ad15f8
commit 12251f960e
41 changed files with 1854 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
lib/pervasives.epi Normal file
View file

@ -0,0 +1,26 @@
(* the core module *)
(* $Id: pervasives.epi 77 2009-03-11 16:07:00Z delaval $ *)
(* pour debugger set arguments -nopervasives -i lib/pervasives.epi *)
type bool = true | false
type int
type float
val fun (&)(bool;bool) returns (bool)
val fun ( * )(int;int) returns (int)
val fun ( *. )(float;float) returns (float)
val fun (+)(int;int) returns (int)
val fun (+.)(float;float) returns (float)
val fun (-)(int;int) returns (int)
val fun (-.)(float;float) returns (float)
val fun (/)(int;int) returns (int)
val fun (/.)(float;float) returns (float)
val fun (<=)(int;int) returns (bool)
val fun (<)(int;int) returns (bool)
val fun (<>)(int;int) returns (bool)
val fun (=)(int;int) returns (bool)
val fun (>=)(int;int) returns (bool)
val fun (>)(int;int) returns (bool)
val fun (not)(bool) returns (bool)
val fun (or)(bool;bool) returns (bool)
val fun (~-)(int) returns (int)
val fun (~-.)(float) returns (float)

35
test/bad/causality.ept Normal file
View file

@ -0,0 +1,35 @@
(* Causality loop *)
node tr(x,y,z,t:bool) returns (v:bool)
let
v = x or y or z or t;
tel
node f(v:bool) returns (x,y,z,t:bool)
let
(x,y,z,t) = (v,v,v,v);
tel
node c(v:bool) returns (x,y,z,t:bool)
let
(x,y,z,t) = (v,v,v,v);
tel
node j(v:bool) returns (x,y,z,t:bool)
let
(x,y,z,t) = (v,v,v,v);
tel
node g() returns (y:bool)
var x,x1,x2,x3,y1,y2,y3,z,z1,z2,z3,t,t1,t2,t3,v:bool;
let
x = x1 or x2 or x3;
y = y1 or y2 or y3;
z = z1 or z2 or z3;
t = t1 or t2 or t3;
(x1,y1,z1,t1) = f(v);
(x2,y2,z2,t2) = c(v);
(x3,y3,z3,t3) = j(v);
v = tr(x,y,z,t);
tel

5
test/bad/t1.ept Normal file
View file

@ -0,0 +1,5 @@
node f(x:int) returns (y:int)
let
y = x;
x = 0;
tel

29
test/bad/t2.ept Normal file
View file

@ -0,0 +1,29 @@
(* pour debugger
set arguments -I test/good -v test/good/t2.ept *)
node h(x,z,m:int) returns (o:int)
var k:int;
last w: int;
let
automaton
state S1
var r:int;
do
k = m + 2;
r = k + 3;
w = 1 + 2;
until (1 = 0) then S2
| (1 = 2) then S1
unless (2 = k) then S2
state S2
do
k = 2;
until (1 = 0) then S2
end;
present
| (x = 0) do o = pre o + 2
| (x = 2) do o = 4
default do o = 2
end
tel

13
test/bad/t3.ept Normal file
View file

@ -0,0 +1,13 @@
(* Unknown state name *)
node f(x:int) returns (y:int)
let
automaton
state A
do y = 2
until y = 2 then B
state B
do y = 3
until y = 3 then C
end
tel

17
test/bad/t4.ept Normal file
View file

@ -0,0 +1,17 @@
(* Non correct transition *)
node f(x:int) returns (y,z:int)
let
automaton
state A do y = x until y = 2 then B
state B do y = x until y = 2 then A
end;
automaton
state C
do z = y
until z = 3 then D
state D
do z = x
until z = 4 then A
end
tel

20
test/bad/t5.ept Normal file
View file

@ -0,0 +1,20 @@
node f(x:int) returns (y,z:int)
let
automaton
state A
do y = x;
z = 4;
until y = 2 then B
state B
do y = x;
automaton
state C
do z = y
until z = 3 then D
state D
do z = x
until z = 4 then A
end
until y = 2 then A
end;
tel

10
test/bad/t6.ept Normal file
View file

@ -0,0 +1,10 @@
(* This example must be REJECTED because of "if z then...",
whereas z is of type int *)
node h(z: int; x, y: int) returns (o2: int)
var o1, o: int;
let
(o1, o2) = if z then (1, 2) else (3, 4);
o = 0 -> pre o + 2
tel

5
test/bad/t7.ept Normal file
View file

@ -0,0 +1,5 @@
node f(x:int;x:int) returns (y:int)
let
y = x;
tel

11
test/bad/t8-causality.ept Normal file
View file

@ -0,0 +1,11 @@
(* Must be rejected because of o1 = o1 + 2 equation (causality error) *)
node f(x,z:int) returns (o1,o2:int)
var o4:int;
let
switch (x = z)
| true do o1 = o1 + 2;o2 = o4+1;o4 = 3
| false do o1 = 4;o2 = 5;o4 = 5
end;
tel

347
test/check Executable file
View file

@ -0,0 +1,347 @@
#!/bin/bash
# $Id$
shopt -s nullglob
# script de test
compilo=../compiler/hec.byte
coption=
# compilateurs utilises pour les tests de gen. de code
CAMLC=ocamlc
JAVAC=javac
LUSTREC=lustre
CC=gcc
MLC=mlc
VHDLC=ghdl
# par defaut : pas de test de generation de code
caml=0
java=0
lustre=0
c=0
cold=0
minils=0
vhdl=0
score=0
max=0
verbose=0
for d in good bad; do
rm -f -r $d/*.obc $d/*_java $d/*_c $d/*_c-old\
$d/*.mci $d/*.mls $d/*.epci\
$d/*.lus $d/*.ml $d/*.cmi $d/*.cmo;
done
#rm -f inline/good/*.ml inline/good/*.cmi inline/good/*.cmo \
# inline/good/*.dcc inline/good/*.lci inline/good/a.out
#../util/split sujet1/bad/bad.split
#../util/split sujet1/good/good.split
compile () {
if [[ $verbose != 0 ]]; then
echo Compile -i $coption $1 $2
$compilo $coption -I good $1 $2;
else
$compilo $coption -I good $1 $2 > /dev/null 2>&1;
fi;
}
launch_check () {
score=0
max=0
echo "Test"
# les mauvais
echo -n "mauvais "
for f in bad/*.ept ; do
echo -n ".";
max=`expr $max + 1`;
if compile $f; then
echo
echo "ECHEC sur "$f" (devrait echouer)";
else
score=`expr $score + 1`;
fi
done
echo
echo -n "bons"
for f in good/*.ept; do
echec=0
echo -n ".";
max=`expr $max + 1`;
base_f=`basename $f .ept`
if compile $f; then
echec=0
else
echec=1
fi
# Compil. minils ?
if [[ ($echec == 0) && ($minils == 1) ]]; then
if $MLC good/${base_f}.mls > /dev/null 2>&1; then
echec=0
else
echec=2
fi
fi
# Compil. caml ?
if [[ ($echec == 0) && ($caml == 1) ]]; then
if $CAMLC -i good/${base_f}.ml > /dev/null; then
echec=0
else
echec=2
fi
fi
# Compil. java ?
if [[ ($echec == 0) && ($java == 1) ]]; then
pushd "good/${base_f}" > /dev/null
for java_file in *.java ; do
if $JAVAC -warn:-unused -sourcepath .:..:../t1 ${java_file} > /dev/null; then
echec=${echec}
else
echec=3
fi
done
popd > /dev/null
fi
# Compil. lustre ?
if [[ ($echec == 0) && ($lustre == 1) ]]; then
if $LUSTREC good/${base_f}.lus > /dev/null; then
echec=0
else
echec=4
fi
fi
# Compil. c ?
if [[ ($echec == 0) && ($c == 1) ]]; then
pushd "good/${base_f}_c" > /dev/null
for c_file in *.c ; do
if $CC -I ../t1_c -c ${c_file} > /dev/null 2>&1; then
echec=${echec}
else
echec=5
fi
done
popd > /dev/null
fi
# Compil. c-old ?
if [[ ($echec == 0) && ($cold == 1) ]]; then
pushd "good/${base_f}_c-old" > /dev/null
for c_file in *.c ; do
if $CC -I ../t1_c-ng -c ${c_file} > /dev/null 2>&1; then
echec=${echec}
else
echec=6
fi
done
popd > /dev/null
fi
if [[ ($echec == 0) && ($vhdl == 1) ]]; then
pushd "good/${base_f}_vhdl" > /dev/null
for vhdl_file in *.vhd; do
if $VHDLC -a ${vhdl_file} && $VHDLC -e ${vhdl_file} > /dev/null 2>&1
then
echec=${echec}
else
echec=7
fi
done
fi
if [[ $echec == 0 ]]; then
score=`expr $score + 1`;
else
echo
echo "ECHEC sur "$f" (devrait reussir)";
case $echec in
1 )
echo "Echec de la compil. vers code objet";;
2 )
echo "Echec de la compil. caml";;
3 )
echo "Echec de la compil. java";;
4 )
echo "Echec de la compil. lustre";;
5 )
echo "Echec de la compil. c";;
6 )
echo "Echec de la compil. c-ng";;
7 )
echo "Echec de la compil. VHDL";;
esac
fi
done
echo
percent=`expr 100 \* $score / $max`;
echo -n "Test: $score/$max : $percent%";
}
activate_minils () {
minils=1
}
activate_caml () {
caml=1
coption="$coption -target caml"
}
activate_java () {
java=1
coption="$coption -target java"
}
activate_lustre () {
lustre=1
coption="$coption -target lustre"
}
activate_c () {
c=1
coption="$coption -target c"
}
activate_cold () {
cng=1
coption="$coption -target c-old"
}
activate_vhdl () {
vhdl=1
coption="$coption -target vhdl"
}
activate_tomato () {
coption="$coption -tomato"
}
activate_cse () {
coption="$coption -cse"
}
activate_inter () {
coption="$coption -inter"
}
activate_boolean () {
coption="$coption -bool"
}
activate_deadcode () {
coption="$coption -deadcode"
}
activate_all () {
activate_caml
activate_java
activate_lustre
activate_c
activate_cold
activate_vhdl
activate_boolean
activate_deadcode
activate_cse
activate_inter
activate_tomato
}
# -1, -2, -3, -v1, -v2, -v3 kept for backward compatibility
# (to be suppressed)
while [ $# -gt 0 ]; do
case $1 in
"-1" )
shift;;
"-2" )
activate_minils
shift;;
"-3" )
activate_minils
shift;;
"-v" )
verbose=1;
shift;;
"-all" )
activate_all
shift;;
"-caml" )
activate_caml
shift;;
"-java" )
activate_java
shift;;
"-lustre" )
activate_lustre
shift;;
"-tomato" )
activate_tomato
shift;;
"-cse" )
activate_cse
shift;;
"-inter" )
activate_inter
shift;;
"-c" )
activate_c
shift;;
"-c-old" )
activate_cold
shift;;
"-vhdl" )
activate_vhdl
shift;;
"-mls" )
activate_minils
shift;;
"-bool" )
activate_boolean
shift;;
"-deadcode" )
activate_deadcode
shift;;
"-v1" )
verbose=1;
shift;;
"-v2" )
verbose=1;
activate_minils
shift;;
"-v3" )
verbose=1;
shift;;
"-h" )
echo "usage : $0 <options> <compilo>"
echo "options : "
echo "-caml : test of code generation (caml code)"
echo "-java : test of code generation (java code)"
echo "-lustre : test of code generation (lustre code)"
echo "-c : test of code generation (c code)"
echo "-c-old : test of code generation (c code, old backend)"
echo "-vhdl : test of code generation (vhdl)"
echo "-bool : test of boolean translation"
echo "-deadcode : test of deadcode removal"
echo "-inter : test of intermediate equations removal"
echo "-tomato : test of automata minimization"
echo "-cse : test of common sub-expression elimination"
echo "-all : test all"
echo "-v : verbose"
exit 0;;
* )
compilo=$1
shift
coption="$coption $*"
break
esac
done
launch_check
echo

33
test/good/alloc.ept Normal file
View file

@ -0,0 +1,33 @@
(* Ressource allocator for two clients, 0 and 1 *)
(* ri means that client i asks for the resource. *)
(* gi means that client i was granted the resource. *)
(* Security property: not (r0 & r1) *)
(* Liveness property (expressed in LTL): G (ri => F gi) *)
node alloc(r0 : bool; r1 : bool) returns (g0 : bool; g1 : bool)
let
automaton
state IDLE0
do g0 = false;
g1 = false;
unless r0 then ALLOC0 | (r1 & not r0) then ALLOC1
state IDLE1
do g0 = false;
g1 = false;
unless r1 then ALLOC1 | (r0 & not r1) then ALLOC0
state ALLOC0
do g0 = true;
g1 = false;
unless (not r0) then IDLE1
state ALLOC1
do g0 = false;
g1 = true;
unless (not r1) then IDLE0
end;
tel

4
test/good/counter.ept Normal file
View file

@ -0,0 +1,4 @@
node counter(res: bool; tick: bool) returns (o: int)
let
o = if res then 0 else if tick then 1 -> pre o + 1 else 0 -> pre o;
tel

12
test/good/norm.ept Normal file
View file

@ -0,0 +1,12 @@
(* pour debugger ../../compiler/hec.byte -i -v -I ../../lib norm.ept *)
(* pour debugger
directory parsing global analysis dataflow sequential sigali simulation translation main
set arguments -v ../test/good/norm.ept *)
(* revoir la fonction de normalisation des when/merge *)
(* il faut que (e when c) soit une action si e est une action *)
node m0() returns (o: int)
let
o = if true then if true then 1 else 2 else 3;
tel

529
test/good/prog20.ept Normal file
View file

@ -0,0 +1,529 @@
node ntasks(r1,s1,r2,s2,r3,s3,r4,s4,r5,s5,r6,s6,r7,s7,r8,s8,r9,s9,r10,s10,r11,s11,r12,s12,r13,s13,r14,s14,r15,s15,r16,s16,r17,s17,r18,s18,r19,s19,r20,s20,r21,s21,r22,s22,r23,s23,r24,s24,r25,s25,r26,s26,r27,s27,r28,s28,r29,s29,r30,s30,r31,s31,r32,s32,r33,s33,r34,s34,r35,s35,r36,s36,r37,s37,r38,s38,r39,s39,r40,s40,r41,s41,r42,s42,r43,s43,r44,s44,r45,s45,r46,s46,r47,s47,r48,s48,r49,s49,r50,s50,r51,s51,r52,s52,r53,s53,r54,s54,r55,s55,r56,s56,r57,s57,r58,s58,r59,s59,r60,s60:bool) returns (a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24,a25,a26,a27,a28,a29,a30,a31,a32,a33,a34,a35,a36,a37,a38,a39,a40,a41,a42,a43,a44,a45,a46,a47,a48,a49,a50,a51,a52,a53,a54,a55,a56,a57,a58,a59,a60:bool)
contract
var err,err1,err2,err3,err4,err5,err6,err7,err8,err9,err10,err11,err12,err13,err14,err15,err16,err17,err18,err19,err20,err21,err22,err23,err24,err25,err26,err27,err28,err29,err30,err31,err32,err33,err34,err35,err36,err37,err38,err39,err40,err41,err42,err43,err44,err45,err46,err47,err48,err49,err50,err51,err52,err53,err54,err55,err56,err57,err58,err59:bool;
let
err = err1 or err2 or err3 or err4 or err5 or err6 or err7 or err8 or err9 or err10 or err11 or err12 or err13 or err14 or err15 or err16 or err17 or err18 or err19;
err1 = a1 & (a2 or a3 or a4 or a5 or a6 or a7 or a8 or a9 or a10 or a11 or a12 or a13 or a14 or a15 or a16 or a17 or a18 or a19 or a20 or a21 or a22 or a23 or a24 or a25 or a26 or a27 or a28 or a29 or a30 or a31 or a32 or a33 or a34 or a35 or a36 or a37 or a38 or a39 or a40 or a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err2 = a2 & (a3 or a4 or a5 or a6 or a7 or a8 or a9 or a10 or a11 or a12 or a13 or a14 or a15 or a16 or a17 or a18 or a19 or a20 or a21 or a22 or a23 or a24 or a25 or a26 or a27 or a28 or a29 or a30 or a31 or a32 or a33 or a34 or a35 or a36 or a37 or a38 or a39 or a40 or a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err3 = a3 & (a4 or a5 or a6 or a7 or a8 or a9 or a10 or a11 or a12 or a13 or a14 or a15 or a16 or a17 or a18 or a19 or a20 or a21 or a22 or a23 or a24 or a25 or a26 or a27 or a28 or a29 or a30 or a31 or a32 or a33 or a34 or a35 or a36 or a37 or a38 or a39 or a40 or a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err4 = a4 & (a5 or a6 or a7 or a8 or a9 or a10 or a11 or a12 or a13 or a14 or a15 or a16 or a17 or a18 or a19 or a20 or a21 or a22 or a23 or a24 or a25 or a26 or a27 or a28 or a29 or a30 or a31 or a32 or a33 or a34 or a35 or a36 or a37 or a38 or a39 or a40 or a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err5 = a5 & (a6 or a7 or a8 or a9 or a10 or a11 or a12 or a13 or a14 or a15 or a16 or a17 or a18 or a19 or a20 or a21 or a22 or a23 or a24 or a25 or a26 or a27 or a28 or a29 or a30 or a31 or a32 or a33 or a34 or a35 or a36 or a37 or a38 or a39 or a40 or a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err6 = a6 & (a7 or a8 or a9 or a10 or a11 or a12 or a13 or a14 or a15 or a16 or a17 or a18 or a19 or a20 or a21 or a22 or a23 or a24 or a25 or a26 or a27 or a28 or a29 or a30 or a31 or a32 or a33 or a34 or a35 or a36 or a37 or a38 or a39 or a40 or a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err7 = a7 & (a8 or a9 or a10 or a11 or a12 or a13 or a14 or a15 or a16 or a17 or a18 or a19 or a20 or a21 or a22 or a23 or a24 or a25 or a26 or a27 or a28 or a29 or a30 or a31 or a32 or a33 or a34 or a35 or a36 or a37 or a38 or a39 or a40 or a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err8 = a8 & (a9 or a10 or a11 or a12 or a13 or a14 or a15 or a16 or a17 or a18 or a19 or a20 or a21 or a22 or a23 or a24 or a25 or a26 or a27 or a28 or a29 or a30 or a31 or a32 or a33 or a34 or a35 or a36 or a37 or a38 or a39 or a40 or a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err9 = a9 & (a10 or a11 or a12 or a13 or a14 or a15 or a16 or a17 or a18 or a19 or a20 or a21 or a22 or a23 or a24 or a25 or a26 or a27 or a28 or a29 or a30 or a31 or a32 or a33 or a34 or a35 or a36 or a37 or a38 or a39 or a40 or a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err10 = a10 & (a11 or a12 or a13 or a14 or a15 or a16 or a17 or a18 or a19 or a20 or a21 or a22 or a23 or a24 or a25 or a26 or a27 or a28 or a29 or a30 or a31 or a32 or a33 or a34 or a35 or a36 or a37 or a38 or a39 or a40 or a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err11 = a11 & (a12 or a13 or a14 or a15 or a16 or a17 or a18 or a19 or a20 or a21 or a22 or a23 or a24 or a25 or a26 or a27 or a28 or a29 or a30 or a31 or a32 or a33 or a34 or a35 or a36 or a37 or a38 or a39 or a40 or a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err12 = a12 & (a13 or a14 or a15 or a16 or a17 or a18 or a19 or a20 or a21 or a22 or a23 or a24 or a25 or a26 or a27 or a28 or a29 or a30 or a31 or a32 or a33 or a34 or a35 or a36 or a37 or a38 or a39 or a40 or a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err13 = a13 & (a14 or a15 or a16 or a17 or a18 or a19 or a20 or a21 or a22 or a23 or a24 or a25 or a26 or a27 or a28 or a29 or a30 or a31 or a32 or a33 or a34 or a35 or a36 or a37 or a38 or a39 or a40 or a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err14 = a14 & (a15 or a16 or a17 or a18 or a19 or a20 or a21 or a22 or a23 or a24 or a25 or a26 or a27 or a28 or a29 or a30 or a31 or a32 or a33 or a34 or a35 or a36 or a37 or a38 or a39 or a40 or a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err15 = a15 & (a16 or a17 or a18 or a19 or a20 or a21 or a22 or a23 or a24 or a25 or a26 or a27 or a28 or a29 or a30 or a31 or a32 or a33 or a34 or a35 or a36 or a37 or a38 or a39 or a40 or a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err16 = a16 & (a17 or a18 or a19 or a20 or a21 or a22 or a23 or a24 or a25 or a26 or a27 or a28 or a29 or a30 or a31 or a32 or a33 or a34 or a35 or a36 or a37 or a38 or a39 or a40 or a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err17 = a17 & (a18 or a19 or a20 or a21 or a22 or a23 or a24 or a25 or a26 or a27 or a28 or a29 or a30 or a31 or a32 or a33 or a34 or a35 or a36 or a37 or a38 or a39 or a40 or a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err18 = a18 & (a19 or a20 or a21 or a22 or a23 or a24 or a25 or a26 or a27 or a28 or a29 or a30 or a31 or a32 or a33 or a34 or a35 or a36 or a37 or a38 or a39 or a40 or a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err19 = a19 & (a20 or a21 or a22 or a23 or a24 or a25 or a26 or a27 or a28 or a29 or a30 or a31 or a32 or a33 or a34 or a35 or a36 or a37 or a38 or a39 or a40 or a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err20 = a20 & (a21 or a22 or a23 or a24 or a25 or a26 or a27 or a28 or a29 or a30 or a31 or a32 or a33 or a34 or a35 or a36 or a37 or a38 or a39 or a40 or a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err21 = a21 & (a22 or a23 or a24 or a25 or a26 or a27 or a28 or a29 or a30 or a31 or a32 or a33 or a34 or a35 or a36 or a37 or a38 or a39 or a40 or a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err22 = a22 & (a23 or a24 or a25 or a26 or a27 or a28 or a29 or a30 or a31 or a32 or a33 or a34 or a35 or a36 or a37 or a38 or a39 or a40 or a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err23 = a23 & (a24 or a25 or a26 or a27 or a28 or a29 or a30 or a31 or a32 or a33 or a34 or a35 or a36 or a37 or a38 or a39 or a40 or a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err24 = a24 & (a25 or a26 or a27 or a28 or a29 or a30 or a31 or a32 or a33 or a34 or a35 or a36 or a37 or a38 or a39 or a40 or a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err25 = a25 & (a26 or a27 or a28 or a29 or a30 or a31 or a32 or a33 or a34 or a35 or a36 or a37 or a38 or a39 or a40 or a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err26 = a26 & (a27 or a28 or a29 or a30 or a31 or a32 or a33 or a34 or a35 or a36 or a37 or a38 or a39 or a40 or a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err27 = a27 & (a28 or a29 or a30 or a31 or a32 or a33 or a34 or a35 or a36 or a37 or a38 or a39 or a40 or a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err28 = a28 & (a29 or a30 or a31 or a32 or a33 or a34 or a35 or a36 or a37 or a38 or a39 or a40 or a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err29 = a29 & (a30 or a31 or a32 or a33 or a34 or a35 or a36 or a37 or a38 or a39 or a40 or a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err30 = a30 & (a31 or a32 or a33 or a34 or a35 or a36 or a37 or a38 or a39 or a40 or a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err31 = a31 & (a32 or a33 or a34 or a35 or a36 or a37 or a38 or a39 or a40 or a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err32 = a32 & (a33 or a34 or a35 or a36 or a37 or a38 or a39 or a40 or a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err33 = a33 & (a34 or a35 or a36 or a37 or a38 or a39 or a40 or a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err34 = a34 & (a35 or a36 or a37 or a38 or a39 or a40 or a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err35 = a35 & (a36 or a37 or a38 or a39 or a40 or a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err36 = a36 & (a37 or a38 or a39 or a40 or a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err37 = a37 & (a38 or a39 or a40 or a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err38 = a38 & (a39 or a40 or a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err39 = a39 & (a40 or a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err40 = a40 & (a41 or a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err41 = a41 & (a42 or a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err42 = a42 & (a43 or a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err43 = a43 & (a44 or a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err44 = a44 & (a45 or a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err45 = a45 & (a46 or a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err46 = a46 & (a47 or a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err47 = a47 & (a48 or a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err48 = a48 & (a49 or a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err49 = a49 & (a50 or a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err50 = a50 & (a51 or a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err51 = a51 & (a52 or a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err52 = a52 & (a53 or a54 or a55 or a56 or a57 or a58 or a59 or a60);
err53 = a53 & (a54 or a55 or a56 or a57 or a58 or a59 or a60);
err54 = a54 & (a55 or a56 or a57 or a58 or a59 or a60);
err55 = a55 & (a56 or a57 or a58 or a59 or a60);
err56 = a56 & (a57 or a58 or a59 or a60);
err57 = a57 & (a58 or a59 or a60);
err58 = a58 & (a59 or a60);
err59 = a59 & (a60);
tel
assume true
enforce (not err) with (c1,c2,c3,c4,c5,c6,c7,c8,c9,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c30,c31,c32,c33,c34,c35,c36,c37,c38,c39,c40,c41,c42,c43,c44,c45,c46,c47,c48,c49,c50,c51,c52,c53,c54,c55,c56,c57,c58,c59,c60:bool)
let
automaton
state Idle_1
do a1 = false until (r1 & c1) then Active_1
state Active_1
do a1 = true until s1 then Idle_1
end;
automaton
state Idle_2
do a2 = false until (r2 & c2) then Active_2
state Active_2
do a2 = true until s2 then Idle_2
end;
automaton
state Idle_3
do a3 = false until (r3 & c3) then Active_3
state Active_3
do a3 = true until s3 then Idle_3
end;
automaton
state Idle_4
do a4 = false until (r4 & c4) then Active_4
state Active_4
do a4 = true until s4 then Idle_4
end;
automaton
state Idle_5
do a5 = false until (r5 & c5) then Active_5
state Active_5
do a5 = true until s5 then Idle_5
end;
automaton
state Idle_6
do a6 = false until (r6 & c6) then Active_6
state Active_6
do a6 = true until s6 then Idle_6
end;
automaton
state Idle_7
do a7 = false until (r7 & c7) then Active_7
state Active_7
do a7 = true until s7 then Idle_7
end;
automaton
state Idle_8
do a8 = false until (r8 & c8) then Active_8
state Active_8
do a8 = true until s8 then Idle_8
end;
automaton
state Idle_9
do a9 = false until (r9 & c9) then Active_9
state Active_9
do a9 = true until s9 then Idle_9
end;
automaton
state Idle_10
do a10 = false until (r10 & c10) then Active_10
state Active_10
do a10 = true until s10 then Idle_10
end;
automaton
state Idle_11
do a11 = false until (r11 & c11) then Active_11
state Active_11
do a11 = true until s11 then Idle_11
end;
automaton
state Idle_12
do a12 = false until (r12 & c12) then Active_12
state Active_12
do a12 = true until s12 then Idle_12
end;
automaton
state Idle_13
do a13 = false until (r13 & c13) then Active_13
state Active_13
do a13 = true until s13 then Idle_13
end;
automaton
state Idle_14
do a14 = false until (r14 & c14) then Active_14
state Active_14
do a14 = true until s14 then Idle_14
end;
automaton
state Idle_15
do a15 = false until (r15 & c15) then Active_15
state Active_15
do a15 = true until s15 then Idle_15
end;
automaton
state Idle_16
do a16 = false until (r16 & c16) then Active_16
state Active_16
do a16 = true until s16 then Idle_16
end;
automaton
state Idle_17
do a17 = false until (r17 & c17) then Active_17
state Active_17
do a17 = true until s17 then Idle_17
end;
automaton
state Idle_18
do a18 = false until (r18 & c18) then Active_18
state Active_18
do a18 = true until s18 then Idle_18
end;
automaton
state Idle_19
do a19 = false until (r19 & c19) then Active_19
state Active_19
do a19 = true until s19 then Idle_19
end;
automaton
state Idle_20
do a20 = false until (r20 & c20) then Active_20
state Active_20
do a20 = true until s20 then Idle_20
end;
automaton
state Idle_21
do a21 = false until (r21 & c21) then Active_21
state Active_21
do a21 = true until s21 then Idle_21
end;
automaton
state Idle_22
do a22 = false until (r22 & c22) then Active_22
state Active_22
do a22 = true until s22 then Idle_22
end;
automaton
state Idle_23
do a23 = false until (r23 & c23) then Active_23
state Active_23
do a23 = true until s23 then Idle_23
end;
automaton
state Idle_24
do a24 = false until (r24 & c24) then Active_24
state Active_24
do a24 = true until s24 then Idle_24
end;
automaton
state Idle_25
do a25 = false until (r25 & c25) then Active_25
state Active_25
do a25 = true until s25 then Idle_25
end;
automaton
state Idle_26
do a26 = false until (r26 & c26) then Active_26
state Active_26
do a26 = true until s26 then Idle_26
end;
automaton
state Idle_27
do a27 = false until (r27 & c27) then Active_27
state Active_27
do a27 = true until s27 then Idle_27
end;
automaton
state Idle_28
do a28 = false until (r28 & c28) then Active_28
state Active_28
do a28 = true until s28 then Idle_28
end;
automaton
state Idle_29
do a29 = false until (r29 & c29) then Active_29
state Active_29
do a29 = true until s29 then Idle_29
end;
automaton
state Idle_30
do a30 = false until (r30 & c30) then Active_30
state Active_30
do a30 = true until s30 then Idle_30
end;
automaton
state Idle_31
do a31 = false until (r31 & c31) then Active_31
state Active_31
do a31 = true until s31 then Idle_31
end;
automaton
state Idle_32
do a32 = false until (r32 & c32) then Active_32
state Active_32
do a32 = true until s32 then Idle_32
end;
automaton
state Idle_33
do a33 = false until (r33 & c33) then Active_33
state Active_33
do a33 = true until s33 then Idle_33
end;
automaton
state Idle_34
do a34 = false until (r34 & c34) then Active_34
state Active_34
do a34 = true until s34 then Idle_34
end;
automaton
state Idle_35
do a35 = false until (r35 & c35) then Active_35
state Active_35
do a35 = true until s35 then Idle_35
end;
automaton
state Idle_36
do a36 = false until (r36 & c36) then Active_36
state Active_36
do a36 = true until s36 then Idle_36
end;
automaton
state Idle_37
do a37 = false until (r37 & c37) then Active_37
state Active_37
do a37 = true until s37 then Idle_37
end;
automaton
state Idle_38
do a38 = false until (r38 & c38) then Active_38
state Active_38
do a38 = true until s38 then Idle_38
end;
automaton
state Idle_39
do a39 = false until (r39 & c39) then Active_39
state Active_39
do a39 = true until s39 then Idle_39
end;
automaton
state Idle_40
do a40 = false until (r40 & c40) then Active_40
state Active_40
do a40 = true until s40 then Idle_40
end;
automaton
state Idle_41
do a41 = false
until (r41 & c41) then Active_41
| (r41 & not c41) then Wait_41
state Wait_41
do a41 = false
until c41 then Active_41
state Active_41
do a41 = true until s41 then Idle_41
end;
automaton
state Idle_42
do a42 = false
until (r42 & c42) then Active_42
| (r42 & not c42) then Wait_42
state Wait_42
do a42 = false
until c42 then Active_42
state Active_42
do a42 = true until s42 then Idle_42
end;
automaton
state Idle_43
do a43 = false
until (r43 & c43) then Active_43
| (r43 & not c43) then Wait_43
state Wait_43
do a43 = false
until c43 then Active_43
state Active_43
do a43 = true until s43 then Idle_43
end;
automaton
state Idle_44
do a44 = false
until (r44 & c44) then Active_44
| (r44 & not c44) then Wait_44
state Wait_44
do a44 = false
until c44 then Active_44
state Active_44
do a44 = true until s44 then Idle_44
end;
automaton
state Idle_45
do a45 = false
until (r45 & c45) then Active_45
| (r45 & not c45) then Wait_45
state Wait_45
do a45 = false
until c45 then Active_45
state Active_45
do a45 = true until s45 then Idle_45
end;
automaton
state Idle_46
do a46 = false
until (r46 & c46) then Active_46
| (r46 & not c46) then Wait_46
state Wait_46
do a46 = false
until c46 then Active_46
state Active_46
do a46 = true until s46 then Idle_46
end;
automaton
state Idle_47
do a47 = false
until (r47 & c47) then Active_47
| (r47 & not c47) then Wait_47
state Wait_47
do a47 = false
until c47 then Active_47
state Active_47
do a47 = true until s47 then Idle_47
end;
automaton
state Idle_48
do a48 = false
until (r48 & c48) then Active_48
| (r48 & not c48) then Wait_48
state Wait_48
do a48 = false
until c48 then Active_48
state Active_48
do a48 = true until s48 then Idle_48
end;
automaton
state Idle_49
do a49 = false
until (r49 & c49) then Active_49
| (r49 & not c49) then Wait_49
state Wait_49
do a49 = false
until c49 then Active_49
state Active_49
do a49 = true until s49 then Idle_49
end;
automaton
state Idle_50
do a50 = false
until (r50 & c50) then Active_50
| (r50 & not c50) then Wait_50
state Wait_50
do a50 = false
until c50 then Active_50
state Active_50
do a50 = true until s50 then Idle_50
end;
automaton
state Idle_51
do a51 = false
until (r51 & c51) then Active_51
| (r51 & not c51) then Wait_51
state Wait_51
do a51 = false
until c51 then Active_51
state Active_51
do a51 = true until s51 then Idle_51
end;
automaton
state Idle_52
do a52 = false
until (r52 & c52) then Active_52
| (r52 & not c52) then Wait_52
state Wait_52
do a52 = false
until c52 then Active_52
state Active_52
do a52 = true until s52 then Idle_52
end;
automaton
state Idle_53
do a53 = false
until (r53 & c53) then Active_53
| (r53 & not c53) then Wait_53
state Wait_53
do a53 = false
until c53 then Active_53
state Active_53
do a53 = true until s53 then Idle_53
end;
automaton
state Idle_54
do a54 = false
until (r54 & c54) then Active_54
| (r54 & not c54) then Wait_54
state Wait_54
do a54 = false
until c54 then Active_54
state Active_54
do a54 = true until s54 then Idle_54
end;
automaton
state Idle_55
do a55 = false
until (r55 & c55) then Active_55
| (r55 & not c55) then Wait_55
state Wait_55
do a55 = false
until c55 then Active_55
state Active_55
do a55 = true until s55 then Idle_55
end;
automaton
state Idle_56
do a56 = false
until (r56 & c56) then Active_56
| (r56 & not c56) then Wait_56
state Wait_56
do a56 = false
until c56 then Active_56
state Active_56
do a56 = true until s56 then Idle_56
end;
automaton
state Idle_57
do a57 = false
until (r57 & c57) then Active_57
| (r57 & not c57) then Wait_57
state Wait_57
do a57 = false
until c57 then Active_57
state Active_57
do a57 = true until s57 then Idle_57
end;
automaton
state Idle_58
do a58 = false
until (r58 & c58) then Active_58
| (r58 & not c58) then Wait_58
state Wait_58
do a58 = false
until c58 then Active_58
state Active_58
do a58 = true until s58 then Idle_58
end;
automaton
state Idle_59
do a59 = false
until (r59 & c59) then Active_59
| (r59 & not c59) then Wait_59
state Wait_59
do a59 = false
until c59 then Active_59
state Active_59
do a59 = true until s59 then Idle_59
end;
automaton
state Idle_60
do a60 = false
until (r60 & c60) then Active_60
| (r60 & not c60) then Wait_60
state Wait_60
do a60 = false
until c60 then Active_60
state Active_60
do a60 = true until s60 then Idle_60
end;
tel

176
test/good/t1.ept Normal file
View file

@ -0,0 +1,176 @@
(* pour debugger ../../compiler/hec.byte -i -v -I ../../lib t1.ept *)
(* pour debugger
directory parsing global analysis dataflow sequential sigali simulation translation main
set arguments -v ../test/good/t1.ept *)
node m0() returns (o: int)
let
o = if true then if true then 1 else 2 else 3;
tel
node mm(x: int) returns (o: int)
var last m: int = 0;
let
switch (x = 0)
| true do m = last m + 1; o = m
| false do m = 2; o = m
end
tel
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
node m(x: int) returns (o: int)
var last o' : int = 1;
let
automaton
state I
do o' = 1
unless (last o' = 2) then J
state J
do o' = 3
unless (last o' = 1) then I
end;
o = o';
tel
node h(z: int; x, y: int) returns (o2: int)
var o1, o: int;
let
(o1, o2) = if z<0 then (1, 2) else (3, 4);
o = 0 -> pre o + 2
tel
node i(x, y: int) returns (o: int)
var z, k: int;
let
reset
o = 0 + x + y;
reset
z = 1 + o + 3;
k = z + o + 2
every (x = x)
every (x = y)
tel
node j(x, y: int) returns (o: int)
let
automaton
state I
var z: int;
do o = 1; z = 2
until (o = 2) then J
state J
do o = 2
until (o = 1) then I
end
tel
node (++)(up, down: int) returns (o: int)
var last cpt: int = 42;
let
o = last cpt;
automaton
state Init
var k : int;
do k = 0 -> pre k + 2;
cpt = 0
until
(up = 1) then Up
state Up
do cpt = last cpt + 1
until (down = 1) then Down
| (down = 0) then Up
state Down
do cpt = (last cpt) + 1
until (up = 1) then Up
end;
tel
node f(x: bool) returns (y: bool)
var z: bool;
let
y = x or x & x;
z = true -> if y then not (pre z) else pre z;
tel
(*
let increasing(x) returns (o)
do true -> x >= pre(x) + 1 done
modes(v0) =
last o = v0
when up(x) returns (w)
assume (x >= 0) ensure (w >= 0)
do w = x + last o + 2; o = w + 4 done
when down(x) returns (w)
do w = x - last o + 2; o = w + 2 done
end
val gain : int >
modes last o : int when up: int -> int when down: int -> int
end with { up # down }
let node gain(v0)(up, down) returns (o)
assume (v0 >= 0) & (increasing up)
guaranty (deacreasing o)
last o = 0 in
automaton
state Await
do
unless down then Down(1) | up then Up(1)
state Down(d)
let rec cpt = 1 -> pre cpt + 1 in
do o = last o - d
until (cpt >= 5) then Down(d-5)
until up then Up(1)
state Up(d)
let rec cpt = 1 -> pre cpt + 1 in
do o = last o + d
until (cpt >= 5) then Up(d+5)
until down then Down(1)
state Unreachable
let rec c = 0 + 2 in
var m in
do o = m + 2; m = 3 + c done
end
node g(x, y: int) returns (o: int)
let
o = x ++ y;
tel
node dfby(x)(y) returns (o)
let
o = x fby (x fby y)
tel
node f(x)(y) returns (o)
var last o = x;
let
o = last o + y
tel
val f : int > (int => int)
static x = e in ...
(if c then (fun x -> x + 2) else (fun k -> k + 3))(x+2)
let M(x1,..., xn) =
let y1 = ... in ... let yk = ... in
modes
mem m1 = ...; mem ml = ...;
step (...) returns (...) ...
reset = ...
end
*)

17
test/good/t10.ept Normal file
View file

@ -0,0 +1,17 @@
(* pour debugger
set arguments -v test/good/t10.ept *)
node f(x:int) returns (y:int)
let
y = 2*x;
tel
node g(x:int) returns (y:int)
let
y = 3*x;
tel
node h(x1,x2:int) returns (y:int)
let
y = f(x1) + g(x2)
tel

12
test/good/t11.ept Normal file
View file

@ -0,0 +1,12 @@
(* Unary operators *)
node f(x:bool;y:int) returns (z:int;t:bool)
let
z = ~- y;
t = not x;
tel
node g(a:bool;b:int) returns (z:int;t:bool)
let
(z,t) = f(a,b);
tel

19
test/good/t12.ept Normal file
View file

@ -0,0 +1,19 @@
(*node foo() returns (res: int)
var x, m, r, y : int;
let
x = 0 fby y + 42;
m = 0 fby r + 42;
r = 1 + x;
y = 1 + m;
res = if true then r else y;
tel*)
node bar() returns (res: int)
var x, m, r, y : int;
let
x = 0 fby y + 42;
m = 0 fby r + 42;
r = if x > 50 then 1 + x else 42;
y = if m > 50 then 1 + m else 42;
res = if true then r else y;
tel

24
test/good/t13.ept Normal file
View file

@ -0,0 +1,24 @@
node count(c : int; r : bool) returns (res : int)
let
(* res = c fby (if r then 0 else res + c);*)
res = 0;
tel
node fourth() returns (res : bool)
var tmp : int;
let
tmp = 0 fby (if res then 0 else tmp + 1);
res = tmp = 0;
tel
node foo() returns (res : int)
let
res = 0 fby (3 + res);
tel
(* Unary operators *)
node main() returns (c : int)
let
c = count(foo(), fourth());
tel

14
test/good/t14.ept Normal file
View file

@ -0,0 +1,14 @@
node count(c : int; r : bool) returns (res : int)
let
res = 0 fby (if r then 0 else res + c);
tel
node byfour() returns (res : int)
let
res = 0 fby (res + 4);
tel
node main() returns (c : int)
let
c = count(byfour(), false);
tel

6
test/good/t15.ept Normal file
View file

@ -0,0 +1,6 @@
(* Crashes the pass removing intermediate equations. *)
node foo() returns (res:int)
let
res = if true then 1 else 1;
tel

9
test/good/t16.ept Normal file
View file

@ -0,0 +1,9 @@
(* Normalization produces a new equation "v_1 = v_1" without any checking! *)
node foo() returns (tmt1:int)
var v_1:int; tmt2:int;
let
tmt1 = (1 + tmt2);
tmt2 = 0 fby v_1;
v_1 = tmt1;
tel

7
test/good/t17.ept Normal file
View file

@ -0,0 +1,7 @@
node h(z: bool; x, y: int) returns (o2: int)
var o1, o: int;
let
(o1, o2) = if z then (1, 2) else (3, 4);
o = 0 -> pre o + 2
tel

11
test/good/t18.ept Normal file
View file

@ -0,0 +1,11 @@
node j(x, v_33: bool) returns (o: int)
let
automaton
state I
do o = 1
until (o = 2) then J
state J
do o = 2
until v_33 then I
end
tel

69
test/good/t2.ept Normal file
View file

@ -0,0 +1,69 @@
(* pour debugger
directory parsing global analysis dataflow sequential sigali simulation translation main
set arguments -I ../test/good -v ../test/good/t2.ept *)
type t
type r2
(*node hh(x: int) returns ()
var y, z: int;
let
y = pre z + 1;
z = 0 -> y;
tel
node jj() returns ()
var last k: int;
let
automaton
state S1
do k = 1
until k = 0 then S2
state S2
do k = last k + 1 until k = 1 then S2
end
tel
*)
node g(x: bool) returns (o: bool)
let
o = T1.f(x)
tel
node hhh() returns ()
var last o': int;
let
automaton
state S1
var r: int;
do o' = 1; r = 2
unless last o' = 0 then S1
end
tel
node hh(x,z,m:int) returns (o:int)
var last k:int = 1;
last w: int = 0;
let
automaton
state S1
var r:int;
do
k = m + 2;
r = k + 3;
w = 1 + 2;
until (1 = 0) then S2
| (1 = 2) then S1
unless (2 = last k) then S1
state S2
do
k = 2;
until (1 = 0) then S2
end;(*
present
| (x = 0) do o = pre o + 2
| (x = 2) do o = 4
default do o = 2
end *) o = 1
tel

39
test/good/t2open.ept Normal file
View file

@ -0,0 +1,39 @@
(* pour debugger
set arguments -I test/good -v test/good/t2.ept *)
open T1
type t
type r2
node g(x: bool) returns (o: bool)
let
o = f(x)
tel
node h(x,z,m:int) returns (o:int)
var last k:int = 0;
last w: int;
let
automaton
state S1
var r:int;
do
k = m + 2;
r = k + 3;
w = 1 + 2;
until (1 = 0) then S2
| (1 = 2) then S1
unless (2 = last k) then S2
state S2
do
k = 2;
until (1 = 0) then S2
end;
present
| (x = 0) do o = pre o + 2
| (x = 2) do o = 4
default do o = 2
end
tel

22
test/good/t3.ept Normal file
View file

@ -0,0 +1,22 @@
(* pour debugger
set arguments -v test/good/t3.ept *)
node f(x,z:int) returns (o:int)
var o1:int;
let
automaton
state Init
do o = 1 + 2
until (o = 0) then Two
state Two do o = 2 + 3 until (o = 1) then Two
end;
automaton
state One
do o1 = 2
until (o = 2) then One
state Three
do o1 = 3
until (o = 3) then One
end
tel

24
test/good/t4.ept Normal file
View file

@ -0,0 +1,24 @@
(* pour debugger
set arguments -v test/good/t4.ept *)
node f() returns (o:int)
var nat, nat2, r:int;
let
nat = 0 -> pre nat + 1;
reset
nat2 = 0 -> pre nat2 + 1;
reset
r = 0 -> pre r + 1;
every (true -> pre r = 4)
every (true -> pre nat2 = 10);
o = r + nat;
tel
node g(x: int) returns (o: int)
let
automaton
state A do o = 1 until x = 1 then B
state B do o = 0 until x = 1 then A
end
tel

14
test/good/t5.ept Normal file
View file

@ -0,0 +1,14 @@
(* pour debugger
set arguments -v test/good/t1.mls *)
type t
node f(x,z:int) returns (o1:int)
var o: int;
let
present
| (x = 0) do o = 0 -> pre(o+0) + 1
| (z = 2) do o = 4 -> 5
default do o = 2
end;
o1 = o;
tel

10
test/good/t6.ept Normal file
View file

@ -0,0 +1,10 @@
node f(x,z:int) returns (o1,o2:int)
var o4:int;
let
switch (x = z)
| true do o1 = pre o1 + 2;o2 = o4+1;o4 = 3
| false do o1 = 4;o2 = 5;o4 = 5
end;
tel

14
test/good/t7.ept Normal file
View file

@ -0,0 +1,14 @@
(* pour debugger
set arguments -v test/good/t7.ept *)
node f(x,z1:int) returns (o:int)
var last z: int;
last m: int;
r: int;
let
o = (-1);
r = 0 + pre o + 2;
z = last z + 2 + last m;
m = r + 2
tel

24
test/good/t8.ept Normal file
View file

@ -0,0 +1,24 @@
(* pour debugger
set arguments -v test/good/t8.ept *)
type t1 = {x: int; y: int}
type t2 = {z: t1; u: int}
node g(x: t1) returns (o: t1)
let o = x tel
node h(x: t1) returns (o: t1)
let o = g(x) tel
node f(x: t1; z1:t2) returns (o:t2)
var last z: t1;
m: t2;
r: int;
let
o = z1;
m = { z = { y = 2; x = 1 }; u = 3 };
z = { x = 4; y = 2 };
r = m.z.x;
tel

11
test/good/t9.ept Normal file
View file

@ -0,0 +1,11 @@
(* pour debugger
set arguments -v test/good/t9.ept *)
node f(x,z:int) returns (o1,o2:int)
let
switch (x = z)
| true var o'1: int; o'2: int;
do (o'1, o'2) = (1, 2); o1 = o'1; o2 = o'2;
| false do (o2, o1) = (3, 3);
end
tel

22
test/good/test.ept Normal file
View file

@ -0,0 +1,22 @@
node (+)(x,y:int) returns (z:int)
let
automaton
state Up
do z = x + y;
until z > 10 then Down
state Down
do z = x - y;
until z < -10 then Up
end
tel
node updown'() returns (y:int)
let
y = (0 fby y) + 1
tel
node main() returns (y:int)
let
y = updown'();
tel

9
test/good/updown.ept Normal file
View file

@ -0,0 +1,9 @@
node updown(on_off : bool) returns (o : bool)
let
automaton
state Down
do o = false until on_off then Up
state Up
do o = true until on_off then Down
end;
tel

27
tools/hec-c.sh Executable file
View file

@ -0,0 +1,27 @@
#!/bin/sh
# This small helper scripts automates the Heptagon -> C translation.
if [ $# -lt 1 ]
then
echo Usage: $0 file.ept
exit 1
fi
compile=1
if [ $# -gt 2 ];
then
nocompile=0
fi
F=$1
REP=`basename $F .ept`_c
shift
# Compile source file to VHDL, flattening node calls
if [ $compile -eq 1 ]; then
hec.byte $@ -s main -target c $F || exit 1
fi
# Compile it with GCC
cc $REP/*.c -o `basename $F .ept` || exit 1

46
tools/hec-vhdl.sh Executable file
View file

@ -0,0 +1,46 @@
#!/bin/sh
# This small helper scripts automates the Heptagon -> VHDL translation.
# You need GHDL and optionally GTKWave for user-friendly visualization.
if [ $# -lt 1 ]
then
echo Usage: $0 file.ept
exit 1
fi
compile=1
if [ $# -gt 2 ];
then
nocompile=0
fi
F=$1
REP=`basename $F .ept`_vhdl
shift
# Compile source file to VHDL, flattening node calls
if [ $compile -eq 1 ]; then
hec.byte $@ -s main -target vhdl $F > tmp.sh || exit 1
fi
# Display the resulting VHDL code
for i in $REP/*.vhd
do
echo File $i
cat -n $i
done
cd $REP || exit 1
# Properly compile it with GHDL; order matters
sh ../tmp.sh && rm -f ../tmp.sh || exit 1
# Link everything using the generated test-bench
ghdl -e main_tb || exit 1
# Run the simulation for 50 nanoseconds, and output the signals to simu.vcd.
./main_tb --stop-time=12ns --vcd=simu.vcd || exit 1
# Call GTKWave for visualization only if it is not already running.
ps aux | grep -v grep | grep -q gtkwave || gtkwave simu.vcd&

10
tools/hept_pygments/README Normal file
View file

@ -0,0 +1,10 @@
This directory holds an Heptagon lexer for Pygments, a Python-based syntax
highlighting system. It can be used for converting Heptagon source code to
colorful LaTeX or HTML.
To install, just run "python setup.py develop --install-dir=$DIR" where $DIR is
a directory included in your $PYTHONPATH.
For more information, refer to http://pygments.org.
-- Adrien Guatto

100
tools/hept_pygments/hept_pygments/__init__.py Normal file
View file

@ -0,0 +1,100 @@
from pygments.lexer import RegexLexer
from pygments.token import *
class HeptagonLexer(RegexLexer):
name = 'Heptagon'
aliases = ['hept']
filenames = ['*.ept']
tokens = {
'root': [
(r'\(\*.*\*\)', Comment),
(r'node|var', Keyword.Declaration),
(r'open', Keyword.Namespace),
(r'returns|let|tel|automaton|state|until|unless|if|then|else|end',
Keyword),
(r'when|merge|fby|do', Keyword),
(r'present', Keyword.Reserved),
(r'int|bool', Keyword.Type),
(r'pre|\-\>|\+|\-|\/|=|&|not|\*|<=|>=|\^', Operator),
(r'\d+', Number.Integer),
(r' |\t', Whitespace),
(r'\(|\)|;|\||:|,|\]|\[|\.', Punctuation),
(r'true|false', Literal),
(r'[A-Z]\w*', String.Symbol),
(r'\w+', Name)
]
}
class MLSLexer(RegexLexer):
name = 'MiniLS'
aliases = ['mls']
filenames = ['*.mls']
tokens = {
'root': [
(r'\(\*.*\*\)', Comment),
(r'node|var', Keyword.Declaration),
(r'open', Keyword.Namespace),
(r'returns|let|tel|if|then|else|end',
Keyword),
(r'when|merge|fby|do', Keyword),
(r'present', Keyword.Reserved),
(r'int|bool', Keyword.Type),
(r'pre|\-\>|\+|\-|\/|=|&|not|\*|<=|>=|\^', Operator),
(r'\d+', Number.Integer),
(r' |\t', Whitespace),
(r'\(|\)|;|\||:|,|\]|\[|\.', Punctuation),
(r'true|false', Literal),
(r'[A-Z]\w*', String.Symbol),
(r'\w+', Name)
]
}
class ObcLexer(RegexLexer):
name = 'Obc'
aliases = ['obc']
filenames = ['*.obc']
tokens = {
'root': [
(r'--.*\n', Comment),
(r'machine|reset|step|var', Keyword.Declaration),
(r'open', Keyword.Namespace),
(r'switch|case|mem|returns', Keyword),
(r'int|bool', Keyword.Type),
(r'\+|\-|\/|=|&|not', Operator),
(r'\d+', Number.Integer),
(r' |\t', Whitespace),
(r'\(|\)|;|\||:|\{|\}|,', Punctuation),
(r'true|false', Literal),
(r'[A-Z]\w*', String.Symbol),
(r'\w+', Name)
]
}
class VHDLLexer(RegexLexer):
name = 'VHSIC Hardware Description Language'
aliases = ['vhdl']
filenames = ['*.vhd']
tokens = {
'root': [
(r'--.*\n', Comment),
(r'architecture|process|signal|entity|function',
Keyword.Declaration),
(r'library|use', Keyword.Namespace),
(r'returns|begin|end|if|then|else|elsif|when|of', Keyword),
(r'natural|bit|std_ulogic', Keyword.Type),
(r'\+|\-|\/|=|&|not|<=|\.', Operator),
(r'\d+', Number.Integer),
(r' |\t', Whitespace),
(r'\(|\)|;|\||:|\{|\}|,|\'', Punctuation),
(r'true|false', Literal),
(r'[A-Z]\w*', String.Symbol),
(r'\w+', Name)
]
}

22
tools/hept_pygments/setup.py Normal file
View file

@ -0,0 +1,22 @@
# -*- coding: utf-8 -*-
"""
A Pygments lexer for Heptagon
"""
from setuptools import setup
__author__ = 'Adrien Guatto'
setup(
name='Heptagon-Pygments',
version='1.0',
description=__doc__,
author=__author__,
packages=['hept_pygments'],
entry_points='''
[pygments.lexers]
Heptagon = hept_pygments:HeptagonLexer
Obc = hept_pygments:ObcLexer
VHDL = hept_pygments:VHDLLexer
MiniLS = hept_pygments:MLSLexer
'''
)