From 7dfee22b6b261f8d4739cfea6e2dd2746abb55e6 Mon Sep 17 00:00:00 2001 From: Dorel Lucanu Date: Sun, 5 Apr 2015 21:28:45 +0300 Subject: [PATCH] updated the .out files. --- arrays/programs/tests/arrasptr.cink.out | 6 +- arrays/programs/tests/callbyval3.cink.out | 8 +- arrays/programs/tests/matrix.cink.out | 6 +- arrays/programs/tests/matrix3d.cink.out | 6 +- .../programs/tests/arrasptr1.cink.out | 6 +- .../programs/tests/arruni1.cink.out | 6 +- .../programs/tests/callbyval1.cink.out | 8 +- .../programs/tests/callbyval2.cink.out | 8 +- basic/programs/tests/assign.cink.out | 6 +- basic/programs/tests/bool.cink.out | 6 +- basic/programs/tests/boolv.cink.out | 6 +- basic/programs/tests/callbyval1.cink.out | 8 +- basic/programs/tests/callbyval2.cink.out | 8 +- basic/programs/tests/comma1.cink.out | 6 +- basic/programs/tests/comma2.cink.out | 6 +- basic/programs/tests/comma3.cink.out | 6 +- basic/programs/tests/comma4.cink.out | 6 +- basic/programs/tests/cout.cink.out | 6 +- basic/programs/tests/doubleprefop.cink.out | 6 +- basic/programs/tests/empty.cink.out | 6 +- basic/programs/tests/io1.cink.out | 6 +- basic/programs/tests/postinc.cink.out | 6 +- basic/programs/tests/prefinc.cink.out | 6 +- ltlmc/programs/peterson-wrong1.cink.out | 704 +++++----- ltlmc/programs/peterson-wrong2.cink.out | 1228 ++++++++--------- pointers/programs/tests/abc.cink.out | 6 +- pointers/programs/tests/dyn1.cink.out | 6 +- pointers/programs/tests/dyn2.cink.out | 8 +- pointers/programs/tests/dyn3.cink.out | 6 +- pointers/programs/tests/indirect.cink.out | 6 +- .../programs/tests/pointersparam.cink.out | 8 +- .../programs/tests/pointersparam2.cink.out | 8 +- pointers/programs/tests/ref1.cink.out | 6 +- references/programs/tests/alias.cink.out | 6 +- references/programs/tests/callbyref.cink.out | 10 +- 35 files changed, 1075 insertions(+), 1075 deletions(-) diff --git a/arrays/programs/tests/arrasptr.cink.out b/arrays/programs/tests/arrasptr.cink.out index 6a1d749..fda2f68 100644 --- a/arrays/programs/tests/arrasptr.cink.out +++ b/arrays/programs/tests/arrasptr.cink.out @@ -25,9 +25,6 @@ main |-> #symScalLoc(1) - - main |-> #symScalLoc(1) - seq-array ( 5 , #symLoc(2) ) |-> store ( store ( store ( store ( store ( const-array ( 5 , 0 ) , 0 , 0 ) , 1 , 2 ) , 2 , 4 ) , 3 , 6 @@ -41,4 +38,7 @@ #symScalLoc(4) |-> 20 #symScalLoc(5) |-> select ( seq-array ( 5 , #symLoc(2) ) , 5 ) + + main |-> #symScalLoc(1) + diff --git a/arrays/programs/tests/callbyval3.cink.out b/arrays/programs/tests/callbyval3.cink.out index a7fa6dd..2e2ca02 100644 --- a/arrays/programs/tests/callbyval3.cink.out +++ b/arrays/programs/tests/callbyval3.cink.out @@ -25,10 +25,6 @@ main |-> #symScalLoc(2) - - f |-> #symScalLoc(1) - main |-> #symScalLoc(2) - seq-array ( 4 , #symLoc(3) ) |-> store ( store ( const-array ( 4 , 0 ) , 1 , 3 ) , 2 , 3 ) @@ -40,4 +36,8 @@ #symScalLoc(4) |-> 3 #symScalLoc(5) |-> 5 + + f |-> #symScalLoc(1) + main |-> #symScalLoc(2) + diff --git a/arrays/programs/tests/matrix.cink.out b/arrays/programs/tests/matrix.cink.out index a87aa87..d9b14f7 100644 --- a/arrays/programs/tests/matrix.cink.out +++ b/arrays/programs/tests/matrix.cink.out @@ -25,9 +25,6 @@ main |-> #symScalLoc(1) - - main |-> #symScalLoc(1) - seq-array ( 2 , #symLoc(2) ) |-> array of 2 array of 3 int select ( seq-array ( 2 , #symLoc(2) ) , 1 ) |-> store ( const-array ( @@ -36,4 +33,7 @@ ]) = 7) ; ((cout << ((a [ 1 ]) [ 2 ])) << (endl)) ; return 0 ; ) + + main |-> #symScalLoc(1) + diff --git a/arrays/programs/tests/matrix3d.cink.out b/arrays/programs/tests/matrix3d.cink.out index 4d4657a..7169541 100644 --- a/arrays/programs/tests/matrix3d.cink.out +++ b/arrays/programs/tests/matrix3d.cink.out @@ -26,9 +26,6 @@ a[0][1][3] = 8 main |-> #symScalLoc(1) - - main |-> #symScalLoc(1) - seq-array ( 2 , #symLoc(2) ) |-> array of 2 array of 3 array of 4 int @@ -45,4 +42,7 @@ a[0][1][3] = 8 (endl)) << "a[0][1][3] = ") ; (cin >> (((a [ 0 ]) [ 1 ]) [ 3 ])) ; ( (cout << (((a [ 0 ]) [ 1 ]) [ 3 ])) << (endl)) ; return 0 ; ) + + main |-> #symScalLoc(1) + diff --git a/arrays/unidimensional/programs/tests/arrasptr1.cink.out b/arrays/unidimensional/programs/tests/arrasptr1.cink.out index a59c072..e5822ac 100644 --- a/arrays/unidimensional/programs/tests/arrasptr1.cink.out +++ b/arrays/unidimensional/programs/tests/arrasptr1.cink.out @@ -24,9 +24,6 @@ i = a[i] = main |-> #symScalLoc(1) - - main |-> #symScalLoc(1) - seq-array ( 5 , #symLoc(2) ) |-> store ( store ( const-array ( 5 , 0 ) , 2 , 5 ) , 3 , 4 ) @@ -37,4 +34,7 @@ i = a[i] = #symScalLoc(3) |-> select ( seq-array ( 5 , #symLoc(2) ) , 3 ) #symScalLoc(4) |-> 2 + + main |-> #symScalLoc(1) + diff --git a/arrays/unidimensional/programs/tests/arruni1.cink.out b/arrays/unidimensional/programs/tests/arruni1.cink.out index a0ff7df..4042d9a 100644 --- a/arrays/unidimensional/programs/tests/arruni1.cink.out +++ b/arrays/unidimensional/programs/tests/arruni1.cink.out @@ -24,9 +24,6 @@ a[5] = 1;1;3 main |-> #symScalLoc(1) - - main |-> #symScalLoc(1) - seq-array ( 5 , #symLoc(2) ) |-> store ( store ( store ( const-array ( 5 , 0 ) , 0 , 1 ) , 3 , 1 ) , 5 , 3 ) @@ -35,4 +32,7 @@ a[5] = 1;1;3 (cout << (a [ 0 ])) << ";") << (a [ 3 ])) << ";") << (a [ 5 ])) ; ) + + main |-> #symScalLoc(1) + diff --git a/arrays/unidimensional/programs/tests/callbyval1.cink.out b/arrays/unidimensional/programs/tests/callbyval1.cink.out index 71601b5..e889a18 100644 --- a/arrays/unidimensional/programs/tests/callbyval1.cink.out +++ b/arrays/unidimensional/programs/tests/callbyval1.cink.out @@ -25,10 +25,6 @@ main |-> #symScalLoc(2) - - f |-> #symScalLoc(1) - main |-> #symScalLoc(2) - seq-array ( 7 , #symLoc(3) ) |-> store ( const-array ( 7 , 0 ) , 3 , 5 ) @@ -39,4 +35,8 @@ #symScalLoc(4) |-> 3 #symScalLoc(5) |-> 5 + + f |-> #symScalLoc(1) + main |-> #symScalLoc(2) + diff --git a/arrays/unidimensional/programs/tests/callbyval2.cink.out b/arrays/unidimensional/programs/tests/callbyval2.cink.out index 214ced4..5d6da61 100644 --- a/arrays/unidimensional/programs/tests/callbyval2.cink.out +++ b/arrays/unidimensional/programs/tests/callbyval2.cink.out @@ -25,10 +25,6 @@ main |-> #symScalLoc(2) - - f |-> #symScalLoc(1) - main |-> #symScalLoc(2) - seq-array ( 7 , #symLoc(3) ) |-> store ( const-array ( 7 , 0 ) , 3 , 5 ) @@ -40,4 +36,8 @@ #symScalLoc(5) |-> 5 #symScalLoc(6) |-> select ( seq-array ( 7 , #symLoc(3) ) , 3 ) + + f |-> #symScalLoc(1) + main |-> #symScalLoc(2) + diff --git a/basic/programs/tests/assign.cink.out b/basic/programs/tests/assign.cink.out index 06235f6..038f193 100644 --- a/basic/programs/tests/assign.cink.out +++ b/basic/programs/tests/assign.cink.out @@ -25,9 +25,6 @@ main |-> #symScalLoc(1) - - main |-> #symScalLoc(1) - #symScalLoc(1) |-> lambda ( @ int x ; int y ; int z ; ((cout << ( (x = 2) + (y = (z = 3)))) << (endl)) ; return 0 ; ) @@ -35,4 +32,7 @@ #symScalLoc(3) |-> 3 #symScalLoc(4) |-> 3 + + main |-> #symScalLoc(1) + diff --git a/basic/programs/tests/bool.cink.out b/basic/programs/tests/bool.cink.out index f97c98b..5313fe9 100644 --- a/basic/programs/tests/bool.cink.out +++ b/basic/programs/tests/bool.cink.out @@ -25,9 +25,6 @@ true main |-> #symScalLoc(1) - - main |-> #symScalLoc(1) - #symScalLoc(1) |-> lambda ( @ int a ; (a = 1) ; int b ; (b = 2) ; int c ; (c = 3) ; if ( (((a < 2) && (b > 1)) || (c > 4)) ) (cout << @@ -36,4 +33,7 @@ true #symScalLoc(3) |-> 2 #symScalLoc(4) |-> 3 + + main |-> #symScalLoc(1) + diff --git a/basic/programs/tests/boolv.cink.out b/basic/programs/tests/boolv.cink.out index 7396fa0..e1ad344 100644 --- a/basic/programs/tests/boolv.cink.out +++ b/basic/programs/tests/boolv.cink.out @@ -25,9 +25,6 @@ x = false main |-> #symScalLoc(1) - - main |-> #symScalLoc(1) - #symScalLoc(1) |-> lambda ( @ bool b ; int x ; (cout << "x = ") ; (cin >> x) ; (b = (x > 5)) ; if ( b ) (cout << "true") ; else (cout @@ -35,4 +32,7 @@ x = false #symScalLoc(2) |-> false #symScalLoc(3) |-> 3 + + main |-> #symScalLoc(1) + diff --git a/basic/programs/tests/callbyval1.cink.out b/basic/programs/tests/callbyval1.cink.out index b6eeb72..b17dfc7 100644 --- a/basic/programs/tests/callbyval1.cink.out +++ b/basic/programs/tests/callbyval1.cink.out @@ -26,10 +26,6 @@ main |-> #symScalLoc(2) - - f |-> #symScalLoc(1) - main |-> #symScalLoc(2) - #symScalLoc(1) |-> lambda ( int x @ int y ; (y = 2) ; return ((x * y) + 1) ; ) @@ -39,4 +35,8 @@ #symScalLoc(4) |-> 3 #symScalLoc(5) |-> 2 + + f |-> #symScalLoc(1) + main |-> #symScalLoc(2) + diff --git a/basic/programs/tests/callbyval2.cink.out b/basic/programs/tests/callbyval2.cink.out index d8efda0..3467478 100644 --- a/basic/programs/tests/callbyval2.cink.out +++ b/basic/programs/tests/callbyval2.cink.out @@ -25,10 +25,6 @@ main |-> #symScalLoc(2) - - f |-> #symScalLoc(1) - main |-> #symScalLoc(2) - #symScalLoc(1) |-> lambda ( int x, bool b @ if ( b ) return (x * 2 ) ; else { } return (x * 3) ; ) @@ -37,4 +33,8 @@ #symScalLoc(3) |-> 5 #symScalLoc(4) |-> false + + f |-> #symScalLoc(1) + main |-> #symScalLoc(2) + diff --git a/basic/programs/tests/comma1.cink.out b/basic/programs/tests/comma1.cink.out index 062ea7f..8174112 100644 --- a/basic/programs/tests/comma1.cink.out +++ b/basic/programs/tests/comma1.cink.out @@ -24,9 +24,6 @@ main |-> #symScalLoc(1) - - main |-> #symScalLoc(1) - #symScalLoc(1) |-> lambda ( @ int i ; (i = 10) ; int b ; (b = 20) ; int c ; (c = 30) ; ((i = b) , c) ; (cout << i) ; (i = (b , c)) ; @@ -35,4 +32,7 @@ #symScalLoc(3) |-> 20 #symScalLoc(4) |-> 30 + + main |-> #symScalLoc(1) + diff --git a/basic/programs/tests/comma2.cink.out b/basic/programs/tests/comma2.cink.out index f4396be..bd33812 100644 --- a/basic/programs/tests/comma2.cink.out +++ b/basic/programs/tests/comma2.cink.out @@ -31,9 +31,6 @@ a=5, b=2, c=3, i=3 main |-> #symScalLoc(1) - - main |-> #symScalLoc(1) - #symScalLoc(1) |-> lambda ( @ int a ; (a = 1) ; int b ; (b = 2) ; int c ; (c = 3) ; int i ; (i = 0) ; (((((((((cout << "a=") << a) << @@ -54,4 +51,7 @@ a=5, b=2, c=3, i=3 #symScalLoc(4) |-> 3 #symScalLoc(5) |-> 3 + + main |-> #symScalLoc(1) + diff --git a/basic/programs/tests/comma3.cink.out b/basic/programs/tests/comma3.cink.out index 4ad227f..f26efa6 100644 --- a/basic/programs/tests/comma3.cink.out +++ b/basic/programs/tests/comma3.cink.out @@ -24,13 +24,13 @@ main |-> #symScalLoc(1) - - main |-> #symScalLoc(1) - #symScalLoc(1) |-> lambda ( @ int i ; int j ; (j = 10) ; (i = ((j = (j + 1)) , ((j + 100) , (999 + j)))) ; (cout << i) ; return 0 ; ) #symScalLoc(2) |-> 1010 #symScalLoc(3) |-> 11 + + main |-> #symScalLoc(1) + diff --git a/basic/programs/tests/comma4.cink.out b/basic/programs/tests/comma4.cink.out index 5151130..64c7687 100644 --- a/basic/programs/tests/comma4.cink.out +++ b/basic/programs/tests/comma4.cink.out @@ -26,9 +26,6 @@ x=6, y=12 main |-> #symScalLoc(1) - - main |-> #symScalLoc(1) - #symScalLoc(1) |-> lambda ( @ int x ; (x = 5) ; int y ; (y = 7) ; (((((cout << "x=") << x) << ", y=") << y) << (endl)) ; (((x = (x + @@ -37,4 +34,7 @@ x=6, y=12 #symScalLoc(2) |-> 6 #symScalLoc(3) |-> 12 + + main |-> #symScalLoc(1) + diff --git a/basic/programs/tests/cout.cink.out b/basic/programs/tests/cout.cink.out index fa13576..f88a336 100644 --- a/basic/programs/tests/cout.cink.out +++ b/basic/programs/tests/cout.cink.out @@ -25,12 +25,12 @@ main |-> #symScalLoc(1) - - main |-> #symScalLoc(1) - #symScalLoc(1) |-> lambda ( @ int a ; (a = 8) ; ((cout << a) << ( endl)) ; ) #symScalLoc(2) |-> 8 + + main |-> #symScalLoc(1) + diff --git a/basic/programs/tests/doubleprefop.cink.out b/basic/programs/tests/doubleprefop.cink.out index a224e2e..22895b0 100644 --- a/basic/programs/tests/doubleprefop.cink.out +++ b/basic/programs/tests/doubleprefop.cink.out @@ -25,9 +25,6 @@ x = 10 5 main |-> #symScalLoc(1) - - main |-> #symScalLoc(1) - #symScalLoc(1) |-> lambda ( @ int z ; int x ; (x = 0) ; (cout << "x = ") ; (cin >> (++ x)) ; (z = ((++ (++ (++ x))) * 2)) ; ((((cout @@ -35,4 +32,7 @@ x = 10 5 #symScalLoc(2) |-> 10 #symScalLoc(3) |-> 5 + + main |-> #symScalLoc(1) + diff --git a/basic/programs/tests/empty.cink.out b/basic/programs/tests/empty.cink.out index 40f440e..b742e61 100644 --- a/basic/programs/tests/empty.cink.out +++ b/basic/programs/tests/empty.cink.out @@ -24,9 +24,6 @@ Hello World! main |-> #symScalLoc(1) - - main |-> #symScalLoc(1) - #symScalLoc(1) |-> lambda ( @ '.Exps(.KList) ; '.Exps(.KList) ; '.Exps(.KList) ; '.Exps(.KList) ; '.Exps(.KList) ; '.Exps(.KList) ; @@ -62,4 +59,7 @@ Hello World! .KList) ; '.Exps(.KList) ; '.Exps(.KList) ; '.Exps(.KList) ; '.Exps( .KList) ; '.Exps(.KList) ; '.Exps(.KList) ; ) + + main |-> #symScalLoc(1) + diff --git a/basic/programs/tests/io1.cink.out b/basic/programs/tests/io1.cink.out index 9eac81d..7754c74 100644 --- a/basic/programs/tests/io1.cink.out +++ b/basic/programs/tests/io1.cink.out @@ -25,9 +25,6 @@ x, y = 45 main |-> #symScalLoc(1) - - main |-> #symScalLoc(1) - #symScalLoc(1) |-> lambda ( @ int x ; int y ; (((cout << "x") << ", y") << " = ") ; ((cin >> x) >> y) ; (((cout << x) << y) << (endl) @@ -35,4 +32,7 @@ x, y = 45 #symScalLoc(2) |-> 4 #symScalLoc(3) |-> 5 + + main |-> #symScalLoc(1) + diff --git a/basic/programs/tests/postinc.cink.out b/basic/programs/tests/postinc.cink.out index efe9c29..9dbc5ea 100644 --- a/basic/programs/tests/postinc.cink.out +++ b/basic/programs/tests/postinc.cink.out @@ -28,9 +28,6 @@ z = 3 main |-> #symScalLoc(1) - - main |-> #symScalLoc(1) - #symScalLoc(1) |-> lambda ( @ int x ; (x = 1) ; int y ; int z ; ( y = (x ++)) ; (((cout << "y = ") << y) << (endl)) ; (z = ((x ++) + ( @@ -41,4 +38,7 @@ z = 3 #symScalLoc(3) |-> 2 #symScalLoc(4) |-> 3 + + main |-> #symScalLoc(1) + diff --git a/basic/programs/tests/prefinc.cink.out b/basic/programs/tests/prefinc.cink.out index 4184157..fc6d946 100644 --- a/basic/programs/tests/prefinc.cink.out +++ b/basic/programs/tests/prefinc.cink.out @@ -25,9 +25,6 @@ x = 2; y = 5 main |-> #symScalLoc(1) - - main |-> #symScalLoc(1) - #symScalLoc(1) |-> lambda ( @ int x ; (x = 1) ; int y ; int z ; ( y = ((++ x) + 3)) ; (((((cout << "x = ") << x) << "; y = ") << y) << @@ -36,4 +33,7 @@ x = 2; y = 5 #symScalLoc(3) |-> 5 #symScalLoc(4) |-> 0 + + main |-> #symScalLoc(1) + diff --git a/ltlmc/programs/peterson-wrong1.cink.out b/ltlmc/programs/peterson-wrong1.cink.out index 1523396..805a7b5 100644 --- a/ltlmc/programs/peterson-wrong1.cink.out +++ b/ltlmc/programs/peterson-wrong1.cink.out @@ -20,12 +20,12 @@ Vertices: ) (std::thread t2 ( peterson2 , '.Exps(.KList) ) ;)) } ~> execute - - .K - noName + + .K + .List @@ -64,12 +64,12 @@ Vertices: '.Exps(.KList) ) ;) (std::thread t2 ( peterson2 , '.Exps( .KList) ) ;)) } ~> execute - - .K - noName + + .K + .List @@ -109,12 +109,12 @@ Vertices: peterson1 , '.Exps(.KList) ) ;) (std::thread t2 ( peterson2 , '.Exps(.KList) ) ;)) } ~> execute - - .K - noName + + .K + .List @@ -149,12 +149,12 @@ Vertices: $lookup ( #symScalLoc(6) ) ~> rvalue ( HOLE ) ~> HOLE ( '.Exps(.KList) ) ~> HOLE ; - - .K - noName + + .K + .List @@ -206,12 +206,12 @@ Vertices: $lookup ( #symScalLoc(4) ) ~> rvalue ( HOLE ) ~> HOLE ( '.Exps(.KList) ) ~> HOLE ; - - .K - t1 + + .K + .List @@ -232,12 +232,12 @@ Vertices: $lookup ( #symScalLoc(5) ) ~> rvalue ( HOLE ) ~> HOLE ( '.Exps(.KList) ) ~> HOLE ; - - .K - t2 + + .K + .List @@ -289,12 +289,12 @@ Vertices: $lookup ( #symScalLoc(5) ) ~> rvalue ( HOLE ) ~> HOLE ( '.Exps(.KList) ) ~> HOLE ; - - .K - t2 + + .K + .List @@ -320,12 +320,12 @@ Vertices: critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -385,12 +385,12 @@ Vertices: critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -419,12 +419,12 @@ Vertices: critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -482,12 +482,12 @@ Vertices: ) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -516,12 +516,12 @@ Vertices: critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -578,12 +578,12 @@ Vertices: while ( (! (turn == 1)) ) { }) ((critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -612,12 +612,12 @@ Vertices: critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -674,12 +674,12 @@ Vertices: ) { }) ((critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -708,12 +708,12 @@ Vertices: critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -773,12 +773,12 @@ Vertices: critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -807,12 +807,12 @@ Vertices: critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -870,12 +870,12 @@ Vertices: ) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -904,12 +904,12 @@ Vertices: critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -966,12 +966,12 @@ Vertices: while ( (! (turn == 2)) ) { }) ((critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -1000,12 +1000,12 @@ Vertices: critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -1062,12 +1062,12 @@ Vertices: ) { }) ((critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -1096,12 +1096,12 @@ Vertices: critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -1158,12 +1158,12 @@ Vertices: ) { }) ((critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -1190,12 +1190,12 @@ Vertices: ) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -1252,12 +1252,12 @@ Vertices: ) { }) ((critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -1283,12 +1283,12 @@ Vertices: while ( (! (turn == 1)) ) { }) ((critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -1354,12 +1354,12 @@ Unlabelled rule [ ) (std::thread t2 ( peterson2 , '.Exps(.KList) ) ;)) } ~> execute - - .K - noName + + .K + .List @@ -1398,12 +1398,12 @@ Unlabelled rule [ '.Exps(.KList) ) ;) (std::thread t2 ( peterson2 , '.Exps( .KList) ) ;)) } ~> execute - - .K - noName + + .K + .List @@ -1445,12 +1445,12 @@ Unlabelled rule [ '.Exps(.KList) ) ;) (std::thread t2 ( peterson2 , '.Exps( .KList) ) ;)) } ~> execute - - .K - noName + + .K + .List @@ -1490,12 +1490,12 @@ Unlabelled rule [ peterson1 , '.Exps(.KList) ) ;) (std::thread t2 ( peterson2 , '.Exps(.KList) ) ;)) } ~> execute - - .K - noName + + .K + .List @@ -1538,12 +1538,12 @@ Unlabelled rule [ peterson1 , '.Exps(.KList) ) ;) (std::thread t2 ( peterson2 , '.Exps(.KList) ) ;)) } ~> execute - - .K - noName + + .K + .List @@ -1578,12 +1578,12 @@ Unlabelled rule [ $lookup ( #symScalLoc(6) ) ~> rvalue ( HOLE ) ~> HOLE ( '.Exps(.KList) ) ~> HOLE ; - - .K - noName + + .K + .List @@ -1636,12 +1636,12 @@ Unlabelled rule [ $lookup ( #symScalLoc(6) ) ~> rvalue ( HOLE ) ~> HOLE ( '.Exps(.KList) ) ~> HOLE ; - - .K - noName + + .K + .List @@ -1693,12 +1693,12 @@ Unlabelled rule [ $lookup ( #symScalLoc(4) ) ~> rvalue ( HOLE ) ~> HOLE ( '.Exps(.KList) ) ~> HOLE ; - - .K - t1 + + .K + .List @@ -1719,12 +1719,12 @@ Unlabelled rule [ $lookup ( #symScalLoc(5) ) ~> rvalue ( HOLE ) ~> HOLE ( '.Exps(.KList) ) ~> HOLE ; - - .K - t2 + + .K + .List @@ -1777,12 +1777,12 @@ Unlabelled rule [ $lookup ( #symScalLoc(4) ) ~> rvalue ( HOLE ) ~> HOLE ( '.Exps(.KList) ) ~> HOLE ; - - .K - t1 + + .K + .List @@ -1803,12 +1803,12 @@ Unlabelled rule [ $lookup ( #symScalLoc(5) ) ~> rvalue ( HOLE ) ~> HOLE ( '.Exps(.KList) ) ~> HOLE ; - - .K - t2 + + .K + .List @@ -1860,12 +1860,12 @@ Unlabelled rule [ $lookup ( #symScalLoc(5) ) ~> rvalue ( HOLE ) ~> HOLE ( '.Exps(.KList) ) ~> HOLE ; - - .K - t2 + + .K + .List @@ -1891,12 +1891,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -1952,12 +1952,12 @@ Unlabelled rule [ $lookup ( #symScalLoc(5) ) ~> rvalue ( HOLE ) ~> HOLE ( '.Exps(.KList) ) ~> HOLE ; - - .K - t2 + + .K + .List @@ -1983,12 +1983,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -2048,12 +2048,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -2082,12 +2082,12 @@ Unlabelled rule [ critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -2148,12 +2148,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -2182,12 +2182,12 @@ Unlabelled rule [ critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -2245,12 +2245,12 @@ Unlabelled rule [ ) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -2279,12 +2279,12 @@ Unlabelled rule [ critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -2343,12 +2343,12 @@ Unlabelled rule [ ) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -2377,12 +2377,12 @@ Unlabelled rule [ critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -2439,12 +2439,12 @@ Unlabelled rule [ while ( (! (turn == 1)) ) { }) ((critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -2473,12 +2473,12 @@ Unlabelled rule [ critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -2536,12 +2536,12 @@ Unlabelled rule [ while ( (! (turn == 1)) ) { }) ((critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -2570,12 +2570,12 @@ Unlabelled rule [ critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -2632,12 +2632,12 @@ Unlabelled rule [ ) { }) ((critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -2666,12 +2666,12 @@ Unlabelled rule [ critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -2729,12 +2729,12 @@ Unlabelled rule [ ) { }) ((critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -2763,12 +2763,12 @@ Unlabelled rule [ critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -2828,12 +2828,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -2862,12 +2862,12 @@ Unlabelled rule [ critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -2928,12 +2928,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -2962,12 +2962,12 @@ Unlabelled rule [ critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -3025,12 +3025,12 @@ Unlabelled rule [ ) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -3059,12 +3059,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -3123,12 +3123,12 @@ Unlabelled rule [ ) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -3157,12 +3157,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -3219,12 +3219,12 @@ Unlabelled rule [ while ( (! (turn == 2)) ) { }) ((critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -3253,12 +3253,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -3316,12 +3316,12 @@ Unlabelled rule [ while ( (! (turn == 2)) ) { }) ((critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -3350,12 +3350,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -3412,12 +3412,12 @@ Unlabelled rule [ ) { }) ((critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -3446,12 +3446,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -3509,12 +3509,12 @@ Unlabelled rule [ ) { }) ((critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -3542,13 +3542,13 @@ Unlabelled rule [ ~> while ( true ) ({ ((((while ( (! (turn == 1)) ) { }) (( critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - - .K - + t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -3605,12 +3605,12 @@ Unlabelled rule [ ) { }) ((critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -3637,12 +3637,12 @@ Unlabelled rule [ ) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -3700,12 +3700,12 @@ Unlabelled rule [ ) { }) ((critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -3732,12 +3732,12 @@ Unlabelled rule [ ) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -3794,12 +3794,12 @@ Unlabelled rule [ ) { }) ((critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -3825,12 +3825,12 @@ Unlabelled rule [ while ( (! (turn == 1)) ) { }) ((critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -3888,12 +3888,12 @@ Unlabelled rule [ ) { }) ((critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -3919,12 +3919,12 @@ Unlabelled rule [ while ( (! (turn == 1)) ) { }) ((critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -3981,12 +3981,12 @@ Unlabelled rule [ while ( (! (turn == 1)) ) { }) ((critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -4015,12 +4015,12 @@ Unlabelled rule [ critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -4078,12 +4078,12 @@ Unlabelled rule [ while ( (! (turn == 1)) ) { }) ((critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -4112,12 +4112,12 @@ Unlabelled rule [ critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -4174,12 +4174,12 @@ Unlabelled rule [ ) { }) ((critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -4208,12 +4208,12 @@ Unlabelled rule [ critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -4271,12 +4271,12 @@ Unlabelled rule [ ) { }) ((critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -4305,12 +4305,12 @@ Unlabelled rule [ critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -4370,12 +4370,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -4404,12 +4404,12 @@ Unlabelled rule [ critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -4470,12 +4470,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -4504,12 +4504,12 @@ Unlabelled rule [ critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -4567,12 +4567,12 @@ Unlabelled rule [ ) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -4601,12 +4601,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -4665,12 +4665,12 @@ Unlabelled rule [ ) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -4699,12 +4699,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -4761,12 +4761,12 @@ Unlabelled rule [ while ( (! (turn == 2)) ) { }) ((critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -4795,12 +4795,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -4858,12 +4858,12 @@ Unlabelled rule [ while ( (! (turn == 2)) ) { }) ((critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -4892,12 +4892,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -4954,12 +4954,12 @@ Unlabelled rule [ ) { }) ((critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -4988,12 +4988,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -5051,12 +5051,12 @@ Unlabelled rule [ ) { }) ((critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -5085,12 +5085,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -5150,12 +5150,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -5184,12 +5184,12 @@ Unlabelled rule [ critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -5250,12 +5250,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -5284,12 +5284,12 @@ Unlabelled rule [ critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -5347,12 +5347,12 @@ Unlabelled rule [ ) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -5381,12 +5381,12 @@ Unlabelled rule [ critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -5445,12 +5445,12 @@ Unlabelled rule [ ) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -5479,12 +5479,12 @@ Unlabelled rule [ critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -5541,12 +5541,12 @@ Unlabelled rule [ while ( (! (turn == 1)) ) { }) ((critical1 = 1) ;)) ((turn = 2) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> @@ -5575,12 +5575,12 @@ Unlabelled rule [ critical2 = 1) ;)) ((turn = 1) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(2) critical2 |-> #symScalLoc(3) main |-> #symScalLoc(6) peterson1 |-> diff --git a/ltlmc/programs/peterson-wrong2.cink.out b/ltlmc/programs/peterson-wrong2.cink.out index 91776bc..af6b9b6 100644 --- a/ltlmc/programs/peterson-wrong2.cink.out +++ b/ltlmc/programs/peterson-wrong2.cink.out @@ -23,12 +23,12 @@ Vertices: , '.Exps(.KList) ) ;) (std::thread t2 ( peterson2 , '.Exps( .KList) ) ;)) } ~> execute - - .K - noName + + .K + .List @@ -71,12 +71,12 @@ Vertices: std::thread t2 ( peterson2 , '.Exps(.KList) ) ;)) } ~> execute - - .K - noName + + .K + .List @@ -120,12 +120,12 @@ Vertices: ) ;) (std::thread t2 ( peterson2 , '.Exps(.KList) ) ;)) } ~> execute - - .K - noName + + .K + .List @@ -170,12 +170,12 @@ Vertices: '.Exps(.KList) ) ;) (std::thread t2 ( peterson2 , '.Exps( .KList) ) ;)) } ~> execute - - .K - noName + + .K + .List @@ -212,12 +212,12 @@ Vertices: $lookup ( #symScalLoc(7) ) ~> rvalue ( HOLE ) ~> HOLE ( '.Exps(.KList) ) ~> HOLE ; - - .K - noName + + .K + .List @@ -274,12 +274,12 @@ Vertices: $lookup ( #symScalLoc(5) ) ~> rvalue ( HOLE ) ~> HOLE ( '.Exps(.KList) ) ~> HOLE ; - - .K - t1 + + .K + .List @@ -301,12 +301,12 @@ Vertices: $lookup ( #symScalLoc(6) ) ~> rvalue ( HOLE ) ~> HOLE ( '.Exps(.KList) ) ~> HOLE ; - - .K - t2 + + .K + .List @@ -363,12 +363,12 @@ Vertices: $lookup ( #symScalLoc(6) ) ~> rvalue ( HOLE ) ~> HOLE ( '.Exps(.KList) ) ~> HOLE ; - - .K - t2 + + .K + .List @@ -396,12 +396,12 @@ Vertices: = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) (( critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -462,12 +462,12 @@ Vertices: $lookup ( #symScalLoc(6) ) ~> rvalue ( HOLE ) ~> HOLE ( '.Exps(.KList) ) ~> HOLE ; - - .K - t2 + + .K + .List @@ -497,12 +497,12 @@ Vertices: critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -569,12 +569,12 @@ Vertices: = 1) ;)) }))) ((critical2 = 1) ;)) ((flag2 = 0) ;)) (( critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -608,12 +608,12 @@ Vertices: critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -682,12 +682,12 @@ Vertices: critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -721,12 +721,12 @@ Vertices: critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -795,12 +795,12 @@ Vertices: critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -833,12 +833,12 @@ Vertices: critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -907,12 +907,12 @@ Vertices: critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -946,12 +946,12 @@ Vertices: )) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -1016,12 +1016,12 @@ Vertices: ) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0 ) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -1055,12 +1055,12 @@ Vertices: )) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -1125,12 +1125,12 @@ Vertices: critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -1164,12 +1164,12 @@ Vertices: )) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -1233,12 +1233,12 @@ Vertices: { })) ((flag1 = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -1272,12 +1272,12 @@ Vertices: )) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -1344,12 +1344,12 @@ Vertices: = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) (( critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -1383,12 +1383,12 @@ Vertices: )) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -1455,12 +1455,12 @@ Vertices: = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) (( critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -1492,12 +1492,12 @@ Vertices: = 1) ;)) }))) ((critical2 = 1) ;)) ((flag2 = 0) ;)) (( critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -1564,12 +1564,12 @@ Vertices: = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) (( critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -1603,12 +1603,12 @@ Vertices: critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -1673,12 +1673,12 @@ Vertices: ) }))) ((critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0 ) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -1710,12 +1710,12 @@ Vertices: = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) (( critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -1780,12 +1780,12 @@ Vertices: critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -1817,12 +1817,12 @@ Vertices: = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) (( critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -1886,12 +1886,12 @@ Vertices: { })) ((flag2 = 1) ;)) }))) ((critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -1923,12 +1923,12 @@ Vertices: = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) (( critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -1992,12 +1992,12 @@ Vertices: { })) ((flag2 = 1) ;)) }))) ((critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -2031,12 +2031,12 @@ Vertices: critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -2100,12 +2100,12 @@ Vertices: { })) ((flag2 = 1) ;)) }))) ((critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -2135,12 +2135,12 @@ Vertices: ) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0 ) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -2205,12 +2205,12 @@ Vertices: ) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0 ) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -2242,12 +2242,12 @@ Vertices: = 1) ;)) }))) ((critical2 = 1) ;)) ((flag2 = 0) ;)) (( critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -2312,12 +2312,12 @@ Vertices: critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -2349,12 +2349,12 @@ Vertices: = 1) ;)) }))) ((critical2 = 1) ;)) ((flag2 = 0) ;)) (( critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -2418,12 +2418,12 @@ Vertices: { })) ((flag1 = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -2455,12 +2455,12 @@ Vertices: = 1) ;)) }))) ((critical2 = 1) ;)) ((flag2 = 0) ;)) (( critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -2524,12 +2524,12 @@ Vertices: { })) ((flag1 = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -2563,12 +2563,12 @@ Vertices: critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -2632,12 +2632,12 @@ Vertices: { })) ((flag1 = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -2667,12 +2667,12 @@ Vertices: ) }))) ((critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0 ) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -2736,12 +2736,12 @@ Vertices: { })) ((flag1 = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -2771,12 +2771,12 @@ Vertices: critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -2851,12 +2851,12 @@ Unlabelled rule [ , '.Exps(.KList) ) ;) (std::thread t2 ( peterson2 , '.Exps( .KList) ) ;)) } ~> execute - - .K - noName + + .K + .List @@ -2899,12 +2899,12 @@ Unlabelled rule [ std::thread t2 ( peterson2 , '.Exps(.KList) ) ;)) } ~> execute - - .K - noName + + .K + .List @@ -2950,12 +2950,12 @@ Unlabelled rule [ std::thread t2 ( peterson2 , '.Exps(.KList) ) ;)) } ~> execute - - .K - noName + + .K + .List @@ -2999,12 +2999,12 @@ Unlabelled rule [ ) ;) (std::thread t2 ( peterson2 , '.Exps(.KList) ) ;)) } ~> execute - - .K - noName + + .K + .List @@ -3051,12 +3051,12 @@ Unlabelled rule [ ) ;) (std::thread t2 ( peterson2 , '.Exps(.KList) ) ;)) } ~> execute - - .K - noName + + .K + .List @@ -3101,12 +3101,12 @@ Unlabelled rule [ '.Exps(.KList) ) ;) (std::thread t2 ( peterson2 , '.Exps( .KList) ) ;)) } ~> execute - - .K - noName + + .K + .List @@ -3154,12 +3154,12 @@ Unlabelled rule [ '.Exps(.KList) ) ;) (std::thread t2 ( peterson2 , '.Exps( .KList) ) ;)) } ~> execute - - .K - noName + + .K + .List @@ -3196,12 +3196,12 @@ Unlabelled rule [ $lookup ( #symScalLoc(7) ) ~> rvalue ( HOLE ) ~> HOLE ( '.Exps(.KList) ) ~> HOLE ; - - .K - noName + + .K + .List @@ -3259,12 +3259,12 @@ Unlabelled rule [ $lookup ( #symScalLoc(7) ) ~> rvalue ( HOLE ) ~> HOLE ( '.Exps(.KList) ) ~> HOLE ; - - .K - noName + + .K + .List @@ -3321,12 +3321,12 @@ Unlabelled rule [ $lookup ( #symScalLoc(5) ) ~> rvalue ( HOLE ) ~> HOLE ( '.Exps(.KList) ) ~> HOLE ; - - .K - t1 + + .K + .List @@ -3348,12 +3348,12 @@ Unlabelled rule [ $lookup ( #symScalLoc(6) ) ~> rvalue ( HOLE ) ~> HOLE ( '.Exps(.KList) ) ~> HOLE ; - - .K - t2 + + .K + .List @@ -3411,12 +3411,12 @@ Unlabelled rule [ $lookup ( #symScalLoc(5) ) ~> rvalue ( HOLE ) ~> HOLE ( '.Exps(.KList) ) ~> HOLE ; - - .K - t1 + + .K + .List @@ -3438,12 +3438,12 @@ Unlabelled rule [ $lookup ( #symScalLoc(6) ) ~> rvalue ( HOLE ) ~> HOLE ( '.Exps(.KList) ) ~> HOLE ; - - .K - t2 + + .K + .List @@ -3500,12 +3500,12 @@ Unlabelled rule [ $lookup ( #symScalLoc(6) ) ~> rvalue ( HOLE ) ~> HOLE ( '.Exps(.KList) ) ~> HOLE ; - - .K - t2 + + .K + .List @@ -3533,12 +3533,12 @@ Unlabelled rule [ = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) (( critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -3600,12 +3600,12 @@ Unlabelled rule [ $lookup ( #symScalLoc(6) ) ~> rvalue ( HOLE ) ~> HOLE ( '.Exps(.KList) ) ~> HOLE ; - - .K - t2 + + .K + .List @@ -3633,12 +3633,12 @@ Unlabelled rule [ = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) (( critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -3699,12 +3699,12 @@ Unlabelled rule [ $lookup ( #symScalLoc(6) ) ~> rvalue ( HOLE ) ~> HOLE ( '.Exps(.KList) ) ~> HOLE ; - - .K - t2 + + .K + .List @@ -3734,12 +3734,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -3801,12 +3801,12 @@ Unlabelled rule [ $lookup ( #symScalLoc(6) ) ~> rvalue ( HOLE ) ~> HOLE ( '.Exps(.KList) ) ~> HOLE ; - - .K - t2 + + .K + .List @@ -3836,12 +3836,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -3908,12 +3908,12 @@ Unlabelled rule [ = 1) ;)) }))) ((critical2 = 1) ;)) ((flag2 = 0) ;)) (( critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -3947,12 +3947,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -4019,13 +4019,13 @@ Unlabelled rule [ ) ({ ((((flag2 = 0) ;) (while ( (flag1 == 1) ) { })) ((flag2 = 1) ;)) }))) ((critical2 = 1) ;)) ((flag2 = 0) ;)) (( critical2 = 0) ;)) }) ~> return noVal ; - - - .K - + t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -4059,12 +4059,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -4133,12 +4133,12 @@ Unlabelled rule [ critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -4172,12 +4172,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -4247,12 +4247,12 @@ Unlabelled rule [ critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -4286,12 +4286,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -4360,12 +4360,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -4398,12 +4398,12 @@ Unlabelled rule [ critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -4473,12 +4473,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -4511,12 +4511,12 @@ Unlabelled rule [ critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -4585,12 +4585,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -4624,12 +4624,12 @@ Unlabelled rule [ )) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -4699,12 +4699,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -4738,12 +4738,12 @@ Unlabelled rule [ )) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -4808,12 +4808,12 @@ Unlabelled rule [ ) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0 ) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -4847,12 +4847,12 @@ Unlabelled rule [ )) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -4918,12 +4918,12 @@ Unlabelled rule [ ) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0 ) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -4957,12 +4957,12 @@ Unlabelled rule [ )) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -5027,12 +5027,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -5066,12 +5066,12 @@ Unlabelled rule [ )) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -5137,12 +5137,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -5176,12 +5176,12 @@ Unlabelled rule [ )) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -5245,12 +5245,12 @@ Unlabelled rule [ { })) ((flag1 = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -5284,12 +5284,12 @@ Unlabelled rule [ )) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -5354,12 +5354,12 @@ Unlabelled rule [ { })) ((flag1 = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -5393,12 +5393,12 @@ Unlabelled rule [ )) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -5465,12 +5465,12 @@ Unlabelled rule [ = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) (( critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -5504,12 +5504,12 @@ Unlabelled rule [ )) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -5577,12 +5577,12 @@ Unlabelled rule [ = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) (( critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -5616,12 +5616,12 @@ Unlabelled rule [ )) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -5688,12 +5688,12 @@ Unlabelled rule [ = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) (( critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -5725,12 +5725,12 @@ Unlabelled rule [ = 1) ;)) }))) ((critical2 = 1) ;)) ((flag2 = 0) ;)) (( critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -5798,12 +5798,12 @@ Unlabelled rule [ = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) (( critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -5835,12 +5835,12 @@ Unlabelled rule [ = 1) ;)) }))) ((critical2 = 1) ;)) ((flag2 = 0) ;)) (( critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -5907,12 +5907,12 @@ Unlabelled rule [ = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) (( critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -5946,12 +5946,12 @@ Unlabelled rule [ critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -6019,12 +6019,12 @@ Unlabelled rule [ = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) (( critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -6058,12 +6058,12 @@ Unlabelled rule [ critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -6128,12 +6128,12 @@ Unlabelled rule [ ) }))) ((critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0 ) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -6165,12 +6165,12 @@ Unlabelled rule [ = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) (( critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -6236,12 +6236,12 @@ Unlabelled rule [ ) }))) ((critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0 ) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -6273,12 +6273,12 @@ Unlabelled rule [ = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) (( critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -6343,12 +6343,12 @@ Unlabelled rule [ critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -6380,12 +6380,12 @@ Unlabelled rule [ = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) (( critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -6451,12 +6451,12 @@ Unlabelled rule [ critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -6488,12 +6488,12 @@ Unlabelled rule [ = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) (( critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -6557,12 +6557,12 @@ Unlabelled rule [ { })) ((flag2 = 1) ;)) }))) ((critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -6594,12 +6594,12 @@ Unlabelled rule [ = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) (( critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -6664,12 +6664,12 @@ Unlabelled rule [ { })) ((flag2 = 1) ;)) }))) ((critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -6701,12 +6701,12 @@ Unlabelled rule [ = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) (( critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -6770,12 +6770,12 @@ Unlabelled rule [ { })) ((flag2 = 1) ;)) }))) ((critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -6809,12 +6809,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -6879,12 +6879,12 @@ Unlabelled rule [ { })) ((flag2 = 1) ;)) }))) ((critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -6918,12 +6918,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -6987,12 +6987,12 @@ Unlabelled rule [ { })) ((flag2 = 1) ;)) }))) ((critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -7022,12 +7022,12 @@ Unlabelled rule [ ) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0 ) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -7092,12 +7092,12 @@ Unlabelled rule [ { })) ((flag2 = 1) ;)) }))) ((critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -7127,12 +7127,12 @@ Unlabelled rule [ ) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0 ) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -7197,12 +7197,12 @@ Unlabelled rule [ ) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0 ) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -7234,12 +7234,12 @@ Unlabelled rule [ = 1) ;)) }))) ((critical2 = 1) ;)) ((flag2 = 0) ;)) (( critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -7305,12 +7305,12 @@ Unlabelled rule [ ) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0 ) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -7342,12 +7342,12 @@ Unlabelled rule [ = 1) ;)) }))) ((critical2 = 1) ;)) ((flag2 = 0) ;)) (( critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -7412,12 +7412,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -7449,12 +7449,12 @@ Unlabelled rule [ = 1) ;)) }))) ((critical2 = 1) ;)) ((flag2 = 0) ;)) (( critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -7520,12 +7520,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -7557,12 +7557,12 @@ Unlabelled rule [ = 1) ;)) }))) ((critical2 = 1) ;)) ((flag2 = 0) ;)) (( critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -7626,12 +7626,12 @@ Unlabelled rule [ { })) ((flag1 = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -7663,12 +7663,12 @@ Unlabelled rule [ = 1) ;)) }))) ((critical2 = 1) ;)) ((flag2 = 0) ;)) (( critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -7733,12 +7733,12 @@ Unlabelled rule [ { })) ((flag1 = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -7770,12 +7770,12 @@ Unlabelled rule [ = 1) ;)) }))) ((critical2 = 1) ;)) ((flag2 = 0) ;)) (( critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -7839,12 +7839,12 @@ Unlabelled rule [ { })) ((flag1 = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -7878,12 +7878,12 @@ Unlabelled rule [ critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -7948,12 +7948,12 @@ Unlabelled rule [ { })) ((flag1 = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -7987,12 +7987,12 @@ Unlabelled rule [ critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -8056,12 +8056,12 @@ Unlabelled rule [ { })) ((flag1 = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -8091,12 +8091,12 @@ Unlabelled rule [ ) }))) ((critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0 ) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -8161,12 +8161,12 @@ Unlabelled rule [ { })) ((flag1 = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -8196,12 +8196,12 @@ Unlabelled rule [ ) }))) ((critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0 ) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -8265,12 +8265,12 @@ Unlabelled rule [ { })) ((flag1 = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -8300,12 +8300,12 @@ Unlabelled rule [ critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -8370,12 +8370,12 @@ Unlabelled rule [ { })) ((flag1 = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -8405,12 +8405,12 @@ Unlabelled rule [ critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -8475,12 +8475,12 @@ Unlabelled rule [ critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -8512,12 +8512,12 @@ Unlabelled rule [ = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) (( critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -8583,12 +8583,12 @@ Unlabelled rule [ critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -8619,13 +8619,13 @@ Unlabelled rule [ ) ({ ((((flag1 = 0) ;) (while ( (flag2 == 1) ) { })) ((flag1 = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) (( critical1 = 0) ;)) }) ~> return noVal ; - - - .K - + t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -8689,12 +8689,12 @@ Unlabelled rule [ { })) ((flag2 = 1) ;)) }))) ((critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -8726,12 +8726,12 @@ Unlabelled rule [ = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) (( critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -8796,12 +8796,12 @@ Unlabelled rule [ { })) ((flag2 = 1) ;)) }))) ((critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -8833,12 +8833,12 @@ Unlabelled rule [ = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) (( critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -8905,12 +8905,12 @@ Unlabelled rule [ = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) (( critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -8942,12 +8942,12 @@ Unlabelled rule [ = 1) ;)) }))) ((critical2 = 1) ;)) ((flag2 = 0) ;)) (( critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -9015,12 +9015,12 @@ Unlabelled rule [ = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) (( critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -9052,12 +9052,12 @@ Unlabelled rule [ = 1) ;)) }))) ((critical2 = 1) ;)) ((flag2 = 0) ;)) (( critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -9124,12 +9124,12 @@ Unlabelled rule [ = 1) ;)) }))) ((critical2 = 1) ;)) ((flag2 = 0) ;)) (( critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -9163,12 +9163,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -9236,12 +9236,12 @@ Unlabelled rule [ = 1) ;)) }))) ((critical2 = 1) ;)) ((flag2 = 0) ;)) (( critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -9275,12 +9275,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -9349,12 +9349,12 @@ Unlabelled rule [ critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -9388,12 +9388,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -9463,12 +9463,12 @@ Unlabelled rule [ critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -9502,12 +9502,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -9576,12 +9576,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -9614,12 +9614,12 @@ Unlabelled rule [ critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -9689,12 +9689,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -9727,12 +9727,12 @@ Unlabelled rule [ critical2 = 1) ;)) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -9801,12 +9801,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -9840,12 +9840,12 @@ Unlabelled rule [ )) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -9915,12 +9915,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -9954,12 +9954,12 @@ Unlabelled rule [ )) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -10024,12 +10024,12 @@ Unlabelled rule [ ) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0 ) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -10063,12 +10063,12 @@ Unlabelled rule [ )) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -10134,12 +10134,12 @@ Unlabelled rule [ ) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0 ) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -10173,12 +10173,12 @@ Unlabelled rule [ )) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -10243,12 +10243,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -10282,12 +10282,12 @@ Unlabelled rule [ )) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -10353,12 +10353,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -10392,12 +10392,12 @@ Unlabelled rule [ )) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -10461,12 +10461,12 @@ Unlabelled rule [ { })) ((flag1 = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -10500,12 +10500,12 @@ Unlabelled rule [ )) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -10570,12 +10570,12 @@ Unlabelled rule [ { })) ((flag1 = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -10609,12 +10609,12 @@ Unlabelled rule [ )) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -10681,12 +10681,12 @@ Unlabelled rule [ = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) (( critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -10720,12 +10720,12 @@ Unlabelled rule [ )) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -10793,12 +10793,12 @@ Unlabelled rule [ = 1) ;)) }))) ((critical1 = 1) ;)) ((flag1 = 0) ;)) (( critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -10832,12 +10832,12 @@ Unlabelled rule [ )) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -10906,12 +10906,12 @@ Unlabelled rule [ critical1 = 1) ;)) ((flag1 = 0) ;)) ((critical1 = 0) ;)) }) ~> return noVal ; - - .K - t1 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> @@ -10945,12 +10945,12 @@ Unlabelled rule [ )) ((flag2 = 0) ;)) ((critical2 = 0) ;)) }) ~> return noVal ; - - .K - t2 + + .K + ( ([ critical1 |-> #symScalLoc(3) critical2 |-> #symScalLoc(4) flag1 |-> #symScalLoc(1) flag2 |-> diff --git a/pointers/programs/tests/abc.cink.out b/pointers/programs/tests/abc.cink.out index 806eab1..90daf3d 100644 --- a/pointers/programs/tests/abc.cink.out +++ b/pointers/programs/tests/abc.cink.out @@ -26,9 +26,6 @@ c = b+1 main |-> #symScalLoc(1) - - main |-> #symScalLoc(1) - #symScalLoc(1) |-> lambda ( @ a of pointer to int ; (a = (new int )) ; b of pointer to int ; (b = (new int)) ; c of pointer to int ; ( @@ -43,4 +40,7 @@ c = b+1 #symScalLoc(6) |-> #symScalLoc(7) #symScalLoc(7) |-> 9 + + main |-> #symScalLoc(1) + diff --git a/pointers/programs/tests/dyn1.cink.out b/pointers/programs/tests/dyn1.cink.out index 8a064a1..f954937 100644 --- a/pointers/programs/tests/dyn1.cink.out +++ b/pointers/programs/tests/dyn1.cink.out @@ -25,9 +25,6 @@ main |-> #symScalLoc(1) - - main |-> #symScalLoc(1) - #symScalLoc(1) |-> lambda ( @ p of pointer to int ; (p = (new int )) ; q of pointer to bool ; (q = (new bool)) ; ((* q) = true) ; if ( @@ -36,4 +33,7 @@ #symScalLoc(3) |-> 7 #symScalLoc(5) |-> true + + main |-> #symScalLoc(1) + diff --git a/pointers/programs/tests/dyn2.cink.out b/pointers/programs/tests/dyn2.cink.out index 2b2234a..1430ed2 100644 --- a/pointers/programs/tests/dyn2.cink.out +++ b/pointers/programs/tests/dyn2.cink.out @@ -26,10 +26,6 @@ main |-> #symScalLoc(2) - - f |-> #symScalLoc(1) - main |-> #symScalLoc(2) - #symScalLoc(1) |-> lambda ( @ p of pointer to int ; (p = (new int )) ; ((* p) = 10) ; return p ; ) @@ -39,4 +35,8 @@ #symScalLoc(4) |-> #symScalLoc(5) #symScalLoc(5) |-> 10 + + f |-> #symScalLoc(1) + main |-> #symScalLoc(2) + diff --git a/pointers/programs/tests/dyn3.cink.out b/pointers/programs/tests/dyn3.cink.out index 8163dbf..713292b 100644 --- a/pointers/programs/tests/dyn3.cink.out +++ b/pointers/programs/tests/dyn3.cink.out @@ -25,9 +25,6 @@ main |-> #symScalLoc(1) - - main |-> #symScalLoc(1) - #symScalLoc(1) |-> lambda ( @ int a ; (a = 10) ; bool b ; (b = true) ; p of pointer to pointer to int ; (p = (new int *)) ; q of @@ -41,4 +38,7 @@ #symScalLoc(6) |-> #symScalLoc(7) #symScalLoc(7) |-> #symScalLoc(3) + + main |-> #symScalLoc(1) + diff --git a/pointers/programs/tests/indirect.cink.out b/pointers/programs/tests/indirect.cink.out index 7464ba3..48a8398 100644 --- a/pointers/programs/tests/indirect.cink.out +++ b/pointers/programs/tests/indirect.cink.out @@ -29,9 +29,6 @@ main |-> #symScalLoc(1) - - main |-> #symScalLoc(1) - #symScalLoc(1) |-> lambda ( @ int x ; y of pointer to int ; z of pointer to pointer to int ; int u ; v of pointer to int ; (y = (& x) @@ -45,4 +42,7 @@ #symScalLoc(5) |-> 20 #symScalLoc(6) |-> #symScalLoc(2) + + main |-> #symScalLoc(1) + diff --git a/pointers/programs/tests/pointersparam.cink.out b/pointers/programs/tests/pointersparam.cink.out index 11649df..e04c58c 100644 --- a/pointers/programs/tests/pointersparam.cink.out +++ b/pointers/programs/tests/pointersparam.cink.out @@ -26,10 +26,6 @@ swap |-> #symScalLoc(1) - - main |-> #symScalLoc(2) - swap |-> #symScalLoc(1) - #symScalLoc(1) |-> lambda ( int (* p), int (* q) @ int a ; (a = (* p)) ; ((* p) = (* q)) ; ((* q) = a) ; ) @@ -45,4 +41,8 @@ #symScalLoc(8) |-> #symScalLoc(4) #symScalLoc(9) |-> 3 + + main |-> #symScalLoc(2) + swap |-> #symScalLoc(1) + diff --git a/pointers/programs/tests/pointersparam2.cink.out b/pointers/programs/tests/pointersparam2.cink.out index b4d7d8d..00ad123 100644 --- a/pointers/programs/tests/pointersparam2.cink.out +++ b/pointers/programs/tests/pointersparam2.cink.out @@ -26,10 +26,6 @@ swap |-> #symScalLoc(1) - - main |-> #symScalLoc(2) - swap |-> #symScalLoc(1) - #symScalLoc(1) |-> lambda ( int (* (* p)), int (* (* q)) @ int a ; (a = (* (* p))) ; ((* (* p)) = (* (* q))) ; ((* (* q)) = a) ; ) @@ -48,4 +44,8 @@ #symScalLoc(10) |-> #symScalLoc(6) #symScalLoc(11) |-> 3 + + main |-> #symScalLoc(2) + swap |-> #symScalLoc(1) + diff --git a/pointers/programs/tests/ref1.cink.out b/pointers/programs/tests/ref1.cink.out index a0679e8..2c12c86 100644 --- a/pointers/programs/tests/ref1.cink.out +++ b/pointers/programs/tests/ref1.cink.out @@ -25,13 +25,13 @@ main |-> #symScalLoc(1) - - main |-> #symScalLoc(1) - #symScalLoc(1) |-> lambda ( @ int a ; (a = 5) ; int x ; (x = (* ( & a))) ; ((cout << x) << (endl)) ; return 0 ; ) #symScalLoc(2) |-> 5 #symScalLoc(3) |-> 5 + + main |-> #symScalLoc(1) + diff --git a/references/programs/tests/alias.cink.out b/references/programs/tests/alias.cink.out index a9d4ac7..5f2f6b5 100644 --- a/references/programs/tests/alias.cink.out +++ b/references/programs/tests/alias.cink.out @@ -25,13 +25,13 @@ main |-> #symScalLoc(1) - - main |-> #symScalLoc(1) - #symScalLoc(1) |-> lambda ( @ int a ; (a = 5) ; b of reference to int ; (b = a) ; (b = 10) ; ((((cout << a) << " ") << b) << (endl)) ; return 0 ; ) #symScalLoc(2) |-> 10 + + main |-> #symScalLoc(1) + diff --git a/references/programs/tests/callbyref.cink.out b/references/programs/tests/callbyref.cink.out index 9dcb902..ff4fd4b 100644 --- a/references/programs/tests/callbyref.cink.out +++ b/references/programs/tests/callbyref.cink.out @@ -28,11 +28,6 @@ x, y: 172 main |-> #symScalLoc(3) - - f |-> #symScalLoc(1) - g |-> #symScalLoc(2) - main |-> #symScalLoc(3) - #symScalLoc(1) |-> lambda ( int x, y of reference to int @ (x = 1) ; (y = 2) ; return x ; ) @@ -47,4 +42,9 @@ x, y: 172 #symScalLoc(6) |-> 1 #symScalLoc(14) |-> 1 + + f |-> #symScalLoc(1) + g |-> #symScalLoc(2) + main |-> #symScalLoc(3) +