From 12251f960ed6d583b703b2ab851c8044f57985aa Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9onard=20G=C3=A9rard?= Date: Mon, 21 Jun 2010 12:11:06 +0200 Subject: [PATCH] Add lib/pervasives.epi, tests, tools --- lib/pervasives.epi | 26 + test/bad/causality.ept | 35 ++ test/bad/t1.ept | 5 + test/bad/t2.ept | 29 + test/bad/t3.ept | 13 + test/bad/t4.ept | 17 + test/bad/t5.ept | 20 + test/bad/t6.ept | 10 + test/bad/t7.ept | 5 + test/bad/t8-causality.ept | 11 + test/check | 347 ++++++++++++ test/good/alloc.ept | 33 ++ test/good/counter.ept | 4 + test/good/norm.ept | 12 + test/good/prog20.ept | 529 ++++++++++++++++++ test/good/t1.ept | 176 ++++++ test/good/t10.ept | 17 + test/good/t11.ept | 12 + test/good/t12.ept | 19 + test/good/t13.ept | 24 + test/good/t14.ept | 14 + test/good/t15.ept | 6 + test/good/t16.ept | 9 + test/good/t17.ept | 7 + test/good/t18.ept | 11 + test/good/t2.ept | 69 +++ test/good/t2open.ept | 39 ++ test/good/t3.ept | 22 + test/good/t4.ept | 24 + test/good/t5.ept | 14 + test/good/t6.ept | 10 + test/good/t7.ept | 14 + test/good/t8.ept | 24 + test/good/t9.ept | 11 + test/good/test.ept | 22 + test/good/updown.ept | 9 + tools/hec-c.sh | 27 + tools/hec-vhdl.sh | 46 ++ tools/hept_pygments/README | 10 + tools/hept_pygments/hept_pygments/__init__.py | 100 ++++ tools/hept_pygments/setup.py | 22 + 41 files changed, 1854 insertions(+) create mode 100644 lib/pervasives.epi create mode 100644 test/bad/causality.ept create mode 100644 test/bad/t1.ept create mode 100644 test/bad/t2.ept create mode 100644 test/bad/t3.ept create mode 100644 test/bad/t4.ept create mode 100644 test/bad/t5.ept create mode 100644 test/bad/t6.ept create mode 100644 test/bad/t7.ept create mode 100644 test/bad/t8-causality.ept create mode 100755 test/check create mode 100644 test/good/alloc.ept create mode 100644 test/good/counter.ept create mode 100644 test/good/norm.ept create mode 100644 test/good/prog20.ept create mode 100644 test/good/t1.ept create mode 100644 test/good/t10.ept create mode 100644 test/good/t11.ept create mode 100644 test/good/t12.ept create mode 100644 test/good/t13.ept create mode 100644 test/good/t14.ept create mode 100644 test/good/t15.ept create mode 100644 test/good/t16.ept create mode 100644 test/good/t17.ept create mode 100644 test/good/t18.ept create mode 100644 test/good/t2.ept create mode 100644 test/good/t2open.ept create mode 100644 test/good/t3.ept create mode 100644 test/good/t4.ept create mode 100644 test/good/t5.ept create mode 100644 test/good/t6.ept create mode 100644 test/good/t7.ept create mode 100644 test/good/t8.ept create mode 100644 test/good/t9.ept create mode 100644 test/good/test.ept create mode 100644 test/good/updown.ept create mode 100755 tools/hec-c.sh create mode 100755 tools/hec-vhdl.sh create mode 100644 tools/hept_pygments/README create mode 100644 tools/hept_pygments/hept_pygments/__init__.py create mode 100644 tools/hept_pygments/setup.py diff --git a/lib/pervasives.epi b/lib/pervasives.epi new file mode 100644 index 0000000..a27b9d4 --- /dev/null +++ b/lib/pervasives.epi @@ -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) + diff --git a/test/bad/causality.ept b/test/bad/causality.ept new file mode 100644 index 0000000..704af2f --- /dev/null +++ b/test/bad/causality.ept @@ -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 + diff --git a/test/bad/t1.ept b/test/bad/t1.ept new file mode 100644 index 0000000..0f9696f --- /dev/null +++ b/test/bad/t1.ept @@ -0,0 +1,5 @@ +node f(x:int) returns (y:int) +let + y = x; + x = 0; +tel diff --git a/test/bad/t2.ept b/test/bad/t2.ept new file mode 100644 index 0000000..a2e4be5 --- /dev/null +++ b/test/bad/t2.ept @@ -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 + diff --git a/test/bad/t3.ept b/test/bad/t3.ept new file mode 100644 index 0000000..b38e668 --- /dev/null +++ b/test/bad/t3.ept @@ -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 diff --git a/test/bad/t4.ept b/test/bad/t4.ept new file mode 100644 index 0000000..4ecf10a --- /dev/null +++ b/test/bad/t4.ept @@ -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 diff --git a/test/bad/t5.ept b/test/bad/t5.ept new file mode 100644 index 0000000..515ed31 --- /dev/null +++ b/test/bad/t5.ept @@ -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 diff --git a/test/bad/t6.ept b/test/bad/t6.ept new file mode 100644 index 0000000..76ad562 --- /dev/null +++ b/test/bad/t6.ept @@ -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 + diff --git a/test/bad/t7.ept b/test/bad/t7.ept new file mode 100644 index 0000000..fdba51d --- /dev/null +++ b/test/bad/t7.ept @@ -0,0 +1,5 @@ +node f(x:int;x:int) returns (y:int) +let + y = x; +tel + diff --git a/test/bad/t8-causality.ept b/test/bad/t8-causality.ept new file mode 100644 index 0000000..f8c040f --- /dev/null +++ b/test/bad/t8-causality.ept @@ -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 + diff --git a/test/check b/test/check new file mode 100755 index 0000000..f7de73a --- /dev/null +++ b/test/check @@ -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 " + 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 diff --git a/test/good/alloc.ept b/test/good/alloc.ept new file mode 100644 index 0000000..d28f59c --- /dev/null +++ b/test/good/alloc.ept @@ -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 \ No newline at end of file diff --git a/test/good/counter.ept b/test/good/counter.ept new file mode 100644 index 0000000..95147c5 --- /dev/null +++ b/test/good/counter.ept @@ -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 diff --git a/test/good/norm.ept b/test/good/norm.ept new file mode 100644 index 0000000..6e4f210 --- /dev/null +++ b/test/good/norm.ept @@ -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 diff --git a/test/good/prog20.ept b/test/good/prog20.ept new file mode 100644 index 0000000..f379dc7 --- /dev/null +++ b/test/good/prog20.ept @@ -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 diff --git a/test/good/t1.ept b/test/good/t1.ept new file mode 100644 index 0000000..069bce3 --- /dev/null +++ b/test/good/t1.ept @@ -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 +*) diff --git a/test/good/t10.ept b/test/good/t10.ept new file mode 100644 index 0000000..4d5196e --- /dev/null +++ b/test/good/t10.ept @@ -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 diff --git a/test/good/t11.ept b/test/good/t11.ept new file mode 100644 index 0000000..3c61f95 --- /dev/null +++ b/test/good/t11.ept @@ -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 + diff --git a/test/good/t12.ept b/test/good/t12.ept new file mode 100644 index 0000000..e8fd52d --- /dev/null +++ b/test/good/t12.ept @@ -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 diff --git a/test/good/t13.ept b/test/good/t13.ept new file mode 100644 index 0000000..499cffb --- /dev/null +++ b/test/good/t13.ept @@ -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 + diff --git a/test/good/t14.ept b/test/good/t14.ept new file mode 100644 index 0000000..4440a29 --- /dev/null +++ b/test/good/t14.ept @@ -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 diff --git a/test/good/t15.ept b/test/good/t15.ept new file mode 100644 index 0000000..ad3287d --- /dev/null +++ b/test/good/t15.ept @@ -0,0 +1,6 @@ +(* Crashes the pass removing intermediate equations. *) + +node foo() returns (res:int) + let + res = if true then 1 else 1; + tel diff --git a/test/good/t16.ept b/test/good/t16.ept new file mode 100644 index 0000000..ba4aa6f --- /dev/null +++ b/test/good/t16.ept @@ -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 diff --git a/test/good/t17.ept b/test/good/t17.ept new file mode 100644 index 0000000..c3b6161 --- /dev/null +++ b/test/good/t17.ept @@ -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 + diff --git a/test/good/t18.ept b/test/good/t18.ept new file mode 100644 index 0000000..d42196f --- /dev/null +++ b/test/good/t18.ept @@ -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 diff --git a/test/good/t2.ept b/test/good/t2.ept new file mode 100644 index 0000000..9f92619 --- /dev/null +++ b/test/good/t2.ept @@ -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 diff --git a/test/good/t2open.ept b/test/good/t2open.ept new file mode 100644 index 0000000..db9fcbc --- /dev/null +++ b/test/good/t2open.ept @@ -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 + diff --git a/test/good/t3.ept b/test/good/t3.ept new file mode 100644 index 0000000..8418e65 --- /dev/null +++ b/test/good/t3.ept @@ -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 + diff --git a/test/good/t4.ept b/test/good/t4.ept new file mode 100644 index 0000000..a89543c --- /dev/null +++ b/test/good/t4.ept @@ -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 + diff --git a/test/good/t5.ept b/test/good/t5.ept new file mode 100644 index 0000000..53688b4 --- /dev/null +++ b/test/good/t5.ept @@ -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 diff --git a/test/good/t6.ept b/test/good/t6.ept new file mode 100644 index 0000000..6fc1826 --- /dev/null +++ b/test/good/t6.ept @@ -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 + diff --git a/test/good/t7.ept b/test/good/t7.ept new file mode 100644 index 0000000..3c99f52 --- /dev/null +++ b/test/good/t7.ept @@ -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 + diff --git a/test/good/t8.ept b/test/good/t8.ept new file mode 100644 index 0000000..11c0db4 --- /dev/null +++ b/test/good/t8.ept @@ -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 + diff --git a/test/good/t9.ept b/test/good/t9.ept new file mode 100644 index 0000000..ea95ed0 --- /dev/null +++ b/test/good/t9.ept @@ -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 diff --git a/test/good/test.ept b/test/good/test.ept new file mode 100644 index 0000000..1fd9d38 --- /dev/null +++ b/test/good/test.ept @@ -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 diff --git a/test/good/updown.ept b/test/good/updown.ept new file mode 100644 index 0000000..5c5ea4d --- /dev/null +++ b/test/good/updown.ept @@ -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 \ No newline at end of file diff --git a/tools/hec-c.sh b/tools/hec-c.sh new file mode 100755 index 0000000..e9e5123 --- /dev/null +++ b/tools/hec-c.sh @@ -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 diff --git a/tools/hec-vhdl.sh b/tools/hec-vhdl.sh new file mode 100755 index 0000000..d850f6c --- /dev/null +++ b/tools/hec-vhdl.sh @@ -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& diff --git a/tools/hept_pygments/README b/tools/hept_pygments/README new file mode 100644 index 0000000..34f7b30 --- /dev/null +++ b/tools/hept_pygments/README @@ -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 diff --git a/tools/hept_pygments/hept_pygments/__init__.py b/tools/hept_pygments/hept_pygments/__init__.py new file mode 100644 index 0000000..6ef48f5 --- /dev/null +++ b/tools/hept_pygments/hept_pygments/__init__.py @@ -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) + ] + } diff --git a/tools/hept_pygments/setup.py b/tools/hept_pygments/setup.py new file mode 100644 index 0000000..37a355f --- /dev/null +++ b/tools/hept_pygments/setup.py @@ -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 + ''' +)