Commit e6b6495e authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Added benchmarks and conversion, running and evaluation scripts

parent 1c8f5fe1
......@@ -13,3 +13,9 @@ cabal-dev
.cabal-sandbox/
cabal.sandbox.config
cabal.config
# Benchmark directory
benchmarks/**/*.pnet
benchmarks/**/*.out
benchmarks/**/*.list
benchmarks/**/*.list.sorted
#!/bin/bash
function sort_file {
cat $1 | \
sed -e 's/^[[:digit:]]* //' \
-e 's/\.pl$//' \
-e 's/\.pnet$//' \
-e 's/\.spec$//' \
-e 's/\.tts$//' | \
sort \
>$1.sorted
}
results_our_tool=( positive negative dontknow error timeout )
results_other_tool=( positive negative error timeout )
our_tool=slapnet
benchmark_dirs=( 'found-in-mist-repo' 'given-by-daniel-kroening' 'ic3-soter' )
benchmark_tools=( 'mist' 'bfc' 'iic' )
for (( benchmark=0;benchmark<${#benchmark_dirs[@]};benchmark++)); do
benchmark_dir='benchmarks/'${benchmark_dirs[$benchmark]}
other_tool=${benchmark_tools[$benchmark]}
echo "$our_tool on $benchmark_dir compared with $other_tool"
for result in "${results_our_tool[@]}"; do
sort_file $benchmark_dir/$result-$our_tool.list
done
for result in "${results_other_tool[@]}"; do
sort_file $benchmark_dir/$result-$other_tool.list
done
echo -n "other\\our| "
for ((rour=0;rour<${#results_our_tool[@]};rour++)); do
printf "%8s | " ${results_our_tool[$rour]}
sums_our_tool[$rour]=0
done
echo
echo -n "---------+-"
for rour in "${results_our_tool[@]}"; do
echo -n "---------+-"
done
echo "---------"
for rother in "${results_other_tool[@]}"; do
printf "%8s | " $rother
sum_other_tool=0
for ((rour=0;rour<${#results_our_tool[@]};rour++)); do
n=`comm -12 $benchmark_dir/${results_our_tool[$rour]}-$our_tool.list.sorted $benchmark_dir/$rother-$other_tool.list.sorted | wc -l`
printf "%8d | " $n
sum_other_tool=$((sum_other_tool + n))
sums_our_tool[$rour]=$((${sums_our_tool[$rour]} + n))
done
printf "%8d\n" $sum_other_tool
done
echo -n "---------+-"
for rour in "${results_our_tool[@]}"; do
echo -n "---------+-"
done
echo "---------"
total_sum=0
echo -n " our sum | "
for ((rour=0;rour<${#results_our_tool[@]};rour++)); do
printf "%8d | " ${sums_our_tool[$rour]}
total_sum=$((total_sum + ${sums_our_tool[$rour]}))
done
printf "%8d\n" $total_sum
echo -n "---------+-"
for rour in "${results_our_tool[@]}"; do
echo -n "---------+-"
done
echo "---------"
total_time=0
echo -n "our time | "
for ((rour=0;rour<${#results_our_tool[@]};rour++)); do
result=${results_our_tool[$rour]}
result_time=0
while read T file; do
result_time=$((result_time + T))
done <$benchmark_dir/$result-$our_tool.list
printf "%1.2e | " $result_time
total_time=$((total_time + $result_time))
done
printf "%1.2e\n" $total_time
echo
done
=====
Description of directories
=====
* ./benchmarks/given-by-daniel-kroening/
* Set corresponding to CProver. CProver uses BFC.
* Taken from: http://www.mpi-sws.org/~jkloos/iic-experiments/cprover.zip
* ./benchmarks/ic3-soter/
* Set corresponding to Soter. Soter uses BFC.
* The examples correspond to Erlang code
* See: http://mjolnir.cs.ox.ac.uk/soter/, http://mjolnir.cs.ox.ac.uk/soter/doc/papers.html
\ No newline at end of file
#!/bin/bash
for spec_file in `find . -name "*.spec"`; do
echo "$spec_file"
cat $spec_file | ./spec-to-petri-net.sh > $spec_file.pnet
done
vars
x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11
rules
x0 >= 1,
x1 >= 1,
x2 >= 1 ->
x0' = x0-1,
x2' = x2-1,
x3' = x3+1;
x0 >= 1,
x1 >= 1,
x2 >= 1 ->
x0' = x0-1,
x1' = x1-1,
x4' = x4+1;
x3 >= 1 ->
x0' = x0+1,
x2' = x2+1,
x3' = x3-1;
x4 >= 1 ->
x0' = x0+1,
x1' = x1+1,
x4' = x4-1;
x0 >= 1,
x5 >= 1,
x6 >= 1 ->
x0' = x0-1,
x6' = x6-1,
x7' = x7+1;
x0 >= 1,
x5 >= 1,
x6 >= 1 ->
x0' = x0-1,
x5' = x5-1,
x8' = x8+1;
x7 >= 1 ->
x0' = x0+1,
x6' = x6+1,
x7' = x7-1;
x8 >= 1 ->
x0' = x0+1,
x5' = x5+1,
x8' = x8-1;
x9 >= 1 ->
x9' = x9-1,
x10' = x10+1;
x10 >= 1 ->
x10' = x10-1,
x11' = x11+1;
x11 >= 1 ->
x11' = x11-1,
x10' = x10+1,
x0' = x0+1;
init
x0 = 0, x1 = 1, x2 = 1, x3 = 0, x4 = 0, x5 = 1, x6 = 1, x7 = 0, x8 = 0, x9 = 1, x10 = 0, x11 = 0
target
x3 >= 1, x4 >= 1
x3 >= 2
x4 >= 2
fms_attic is a different version of FMS whose provenance is unfortunately unknown.
ping pong is a PN model for an asynchronous program (stemming from some tests with M. Emmi).
The bingham_h examples are *contrived* examples whose description is given in
J. Bingham, INFINITY'04. They show some weaknesses of our approach especially
of our data structure which does not scale too well with nets with many places.
Also it shows that ic4pn does not perform well because it has to refine until
almost all places are separated.
On a positive note, bingham_h250_attic has a different target from bingham_h250.
On this example ic4pn terminates with 10 variables.
vars
x0 x1 x2 x3 x4
rules
x0 >= 1,
x1 >= 1,
x2 >= 1 ->
x0' = x0-1,
x2' = x2-1,
x3' = x3+1;
x0 >= 1,
x1 >= 1,
x2 >= 1 ->
x0' = x0-1,
x1' = x1-1,
x4' = x4+1;
x3 >= 1 ->
x0' = x0+1,
x2' = x2+1,
x3' = x3-1;
x4 >= 1 ->
x0' = x0+1,
x1' = x1+1,
x4' = x4-1;
init
x0 >= 1, x1 = 1, x2 = 1, x3 = 0, x4 = 0
target
x3 >= 1, x4 >= 1
x3 >= 2
x4 >= 2
invariants
x0=1, x2=1, x3=2
x0=1, x1=1, x4=2
vars
x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40 x41 x42 x43 x44 x45 x46 x47 x48 x49 x50 x51 x52 x53 x54 x55 x56 x57 x58 x59 x60 x61 x62 x63 x64 x65 x66 x67 x68 x69 x70 x71 x72 x73 x74 x75 x76 x77 x78 x79 x80 x81 x82 x83 x84 x85 x86 x87 x88 x89 x90 x91 x92 x93 x94 x95 x96 x97 x98 x99 x100 x101 x102 x103 x104 x105 x106 x107 x108 x109 x110 x111 x112 x113 x114 x115 x116 x117 x118 x119 x120 x121 x122 x123 x124 x125 x126 x127 x128 x129 x130 x131 x132 x133 x134 x135 x136 x137 x138 x139 x140 x141 x142 x143 x144 x145 x146 x147 x148 x149 x150 x151 x152
rules
x0 >= 1, x152 >= 1 -> x0'=x0-1, x152'=x152-1, x151'=x151+1, x1'=x1+1;
x1 >= 1, x152 >= 1 -> x1'=x1-1, x152'=x152-1, x151'=x151+1, x0'=x0+1;
x1 >= 1, x151 >= 1 -> x1'=x1-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x1 >= 1 -> x1'=x1-1, x2'=x2+1;
x2 >= 1, x151 >= 1 -> x2'=x2-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x2 >= 1 -> x2'=x2-1, x3'=x3+1;
x3 >= 1, x151 >= 1 -> x3'=x3-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x3 >= 1 -> x3'=x3-1, x4'=x4+1;
x4 >= 1, x151 >= 1 -> x4'=x4-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x4 >= 1 -> x4'=x4-1, x5'=x5+1;
x5 >= 1, x151 >= 1 -> x5'=x5-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x5 >= 1 -> x5'=x5-1, x6'=x6+1;
x6 >= 1, x151 >= 1 -> x6'=x6-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x6 >= 1 -> x6'=x6-1, x7'=x7+1;
x7 >= 1, x151 >= 1 -> x7'=x7-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x7 >= 1 -> x7'=x7-1, x8'=x8+1;
x8 >= 1, x151 >= 1 -> x8'=x8-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x8 >= 1 -> x8'=x8-1, x9'=x9+1;
x9 >= 1, x151 >= 1 -> x9'=x9-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x9 >= 1 -> x9'=x9-1, x10'=x10+1;
x10 >= 1, x151 >= 1 -> x10'=x10-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x10 >= 1 -> x10'=x10-1, x11'=x11+1;
x11 >= 1, x151 >= 1 -> x11'=x11-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x11 >= 1 -> x11'=x11-1, x12'=x12+1;
x12 >= 1, x151 >= 1 -> x12'=x12-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x12 >= 1 -> x12'=x12-1, x13'=x13+1;
x13 >= 1, x151 >= 1 -> x13'=x13-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x13 >= 1 -> x13'=x13-1, x14'=x14+1;
x14 >= 1, x151 >= 1 -> x14'=x14-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x14 >= 1 -> x14'=x14-1, x15'=x15+1;
x15 >= 1, x151 >= 1 -> x15'=x15-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x15 >= 1 -> x15'=x15-1, x16'=x16+1;
x16 >= 1, x151 >= 1 -> x16'=x16-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x16 >= 1 -> x16'=x16-1, x17'=x17+1;
x17 >= 1, x151 >= 1 -> x17'=x17-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x17 >= 1 -> x17'=x17-1, x18'=x18+1;
x18 >= 1, x151 >= 1 -> x18'=x18-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x18 >= 1 -> x18'=x18-1, x19'=x19+1;
x19 >= 1, x151 >= 1 -> x19'=x19-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x19 >= 1 -> x19'=x19-1, x20'=x20+1;
x20 >= 1, x151 >= 1 -> x20'=x20-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x20 >= 1 -> x20'=x20-1, x21'=x21+1;
x21 >= 1, x151 >= 1 -> x21'=x21-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x21 >= 1 -> x21'=x21-1, x22'=x22+1;
x22 >= 1, x151 >= 1 -> x22'=x22-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x22 >= 1 -> x22'=x22-1, x23'=x23+1;
x23 >= 1, x151 >= 1 -> x23'=x23-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x23 >= 1 -> x23'=x23-1, x24'=x24+1;
x24 >= 1, x151 >= 1 -> x24'=x24-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x24 >= 1 -> x24'=x24-1, x25'=x25+1;
x25 >= 1, x151 >= 1 -> x25'=x25-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x25 >= 1 -> x25'=x25-1, x26'=x26+1;
x26 >= 1, x151 >= 1 -> x26'=x26-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x26 >= 1 -> x26'=x26-1, x27'=x27+1;
x27 >= 1, x151 >= 1 -> x27'=x27-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x27 >= 1 -> x27'=x27-1, x28'=x28+1;
x28 >= 1, x151 >= 1 -> x28'=x28-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x28 >= 1 -> x28'=x28-1, x29'=x29+1;
x29 >= 1, x151 >= 1 -> x29'=x29-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x29 >= 1 -> x29'=x29-1, x30'=x30+1;
x30 >= 1, x151 >= 1 -> x30'=x30-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x30 >= 1 -> x30'=x30-1, x31'=x31+1;
x31 >= 1, x151 >= 1 -> x31'=x31-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x31 >= 1 -> x31'=x31-1, x32'=x32+1;
x32 >= 1, x151 >= 1 -> x32'=x32-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x32 >= 1 -> x32'=x32-1, x33'=x33+1;
x33 >= 1, x151 >= 1 -> x33'=x33-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x33 >= 1 -> x33'=x33-1, x34'=x34+1;
x34 >= 1, x151 >= 1 -> x34'=x34-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x34 >= 1 -> x34'=x34-1, x35'=x35+1;
x35 >= 1, x151 >= 1 -> x35'=x35-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x35 >= 1 -> x35'=x35-1, x36'=x36+1;
x36 >= 1, x151 >= 1 -> x36'=x36-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x36 >= 1 -> x36'=x36-1, x37'=x37+1;
x37 >= 1, x151 >= 1 -> x37'=x37-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x37 >= 1 -> x37'=x37-1, x38'=x38+1;
x38 >= 1, x151 >= 1 -> x38'=x38-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x38 >= 1 -> x38'=x38-1, x39'=x39+1;
x39 >= 1, x151 >= 1 -> x39'=x39-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x39 >= 1 -> x39'=x39-1, x40'=x40+1;
x40 >= 1, x151 >= 1 -> x40'=x40-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x40 >= 1 -> x40'=x40-1, x41'=x41+1;
x41 >= 1, x151 >= 1 -> x41'=x41-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x41 >= 1 -> x41'=x41-1, x42'=x42+1;
x42 >= 1, x151 >= 1 -> x42'=x42-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x42 >= 1 -> x42'=x42-1, x43'=x43+1;
x43 >= 1, x151 >= 1 -> x43'=x43-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x43 >= 1 -> x43'=x43-1, x44'=x44+1;
x44 >= 1, x151 >= 1 -> x44'=x44-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x44 >= 1 -> x44'=x44-1, x45'=x45+1;
x45 >= 1, x151 >= 1 -> x45'=x45-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x45 >= 1 -> x45'=x45-1, x46'=x46+1;
x46 >= 1, x151 >= 1 -> x46'=x46-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x46 >= 1 -> x46'=x46-1, x47'=x47+1;
x47 >= 1, x151 >= 1 -> x47'=x47-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x47 >= 1 -> x47'=x47-1, x48'=x48+1;
x48 >= 1, x151 >= 1 -> x48'=x48-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x48 >= 1 -> x48'=x48-1, x49'=x49+1;
x49 >= 1, x151 >= 1 -> x49'=x49-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x49 >= 1 -> x49'=x49-1, x50'=x50+1;
x50 >= 1, x151 >= 1 -> x50'=x50-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x50 >= 1 -> x50'=x50-1, x51'=x51+1;
x51 >= 1, x151 >= 1 -> x51'=x51-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x51 >= 1 -> x51'=x51-1, x52'=x52+1;
x52 >= 1, x151 >= 1 -> x52'=x52-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x52 >= 1 -> x52'=x52-1, x53'=x53+1;
x53 >= 1, x151 >= 1 -> x53'=x53-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x53 >= 1 -> x53'=x53-1, x54'=x54+1;
x54 >= 1, x151 >= 1 -> x54'=x54-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x54 >= 1 -> x54'=x54-1, x55'=x55+1;
x55 >= 1, x151 >= 1 -> x55'=x55-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x55 >= 1 -> x55'=x55-1, x56'=x56+1;
x56 >= 1, x151 >= 1 -> x56'=x56-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x56 >= 1 -> x56'=x56-1, x57'=x57+1;
x57 >= 1, x151 >= 1 -> x57'=x57-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x57 >= 1 -> x57'=x57-1, x58'=x58+1;
x58 >= 1, x151 >= 1 -> x58'=x58-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x58 >= 1 -> x58'=x58-1, x59'=x59+1;
x59 >= 1, x151 >= 1 -> x59'=x59-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x59 >= 1 -> x59'=x59-1, x60'=x60+1;
x60 >= 1, x151 >= 1 -> x60'=x60-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x60 >= 1 -> x60'=x60-1, x61'=x61+1;
x61 >= 1, x151 >= 1 -> x61'=x61-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x61 >= 1 -> x61'=x61-1, x62'=x62+1;
x62 >= 1, x151 >= 1 -> x62'=x62-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x62 >= 1 -> x62'=x62-1, x63'=x63+1;
x63 >= 1, x151 >= 1 -> x63'=x63-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x63 >= 1 -> x63'=x63-1, x64'=x64+1;
x64 >= 1, x151 >= 1 -> x64'=x64-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x64 >= 1 -> x64'=x64-1, x65'=x65+1;
x65 >= 1, x151 >= 1 -> x65'=x65-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x65 >= 1 -> x65'=x65-1, x66'=x66+1;
x66 >= 1, x151 >= 1 -> x66'=x66-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x66 >= 1 -> x66'=x66-1, x67'=x67+1;
x67 >= 1, x151 >= 1 -> x67'=x67-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x67 >= 1 -> x67'=x67-1, x68'=x68+1;
x68 >= 1, x151 >= 1 -> x68'=x68-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x68 >= 1 -> x68'=x68-1, x69'=x69+1;
x69 >= 1, x151 >= 1 -> x69'=x69-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x69 >= 1 -> x69'=x69-1, x70'=x70+1;
x70 >= 1, x151 >= 1 -> x70'=x70-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x70 >= 1 -> x70'=x70-1, x71'=x71+1;
x71 >= 1, x151 >= 1 -> x71'=x71-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x71 >= 1 -> x71'=x71-1, x72'=x72+1;
x72 >= 1, x151 >= 1 -> x72'=x72-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x72 >= 1 -> x72'=x72-1, x73'=x73+1;
x73 >= 1, x151 >= 1 -> x73'=x73-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x73 >= 1 -> x73'=x73-1, x74'=x74+1;
x74 >= 1, x151 >= 1 -> x74'=x74-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x74 >= 1 -> x74'=x74-1, x75'=x75+1;
x75 >= 1, x151 >= 1 -> x75'=x75-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x75 >= 1 -> x75'=x75-1, x76'=x76+1;
x76 >= 1, x151 >= 1 -> x76'=x76-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x76 >= 1 -> x76'=x76-1, x77'=x77+1;
x77 >= 1, x151 >= 1 -> x77'=x77-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x77 >= 1 -> x77'=x77-1, x78'=x78+1;
x78 >= 1, x151 >= 1 -> x78'=x78-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x78 >= 1 -> x78'=x78-1, x79'=x79+1;
x79 >= 1, x151 >= 1 -> x79'=x79-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x79 >= 1 -> x79'=x79-1, x80'=x80+1;
x80 >= 1, x151 >= 1 -> x80'=x80-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x80 >= 1 -> x80'=x80-1, x81'=x81+1;
x81 >= 1, x151 >= 1 -> x81'=x81-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x81 >= 1 -> x81'=x81-1, x82'=x82+1;
x82 >= 1, x151 >= 1 -> x82'=x82-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x82 >= 1 -> x82'=x82-1, x83'=x83+1;
x83 >= 1, x151 >= 1 -> x83'=x83-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x83 >= 1 -> x83'=x83-1, x84'=x84+1;
x84 >= 1, x151 >= 1 -> x84'=x84-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x84 >= 1 -> x84'=x84-1, x85'=x85+1;
x85 >= 1, x151 >= 1 -> x85'=x85-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x85 >= 1 -> x85'=x85-1, x86'=x86+1;
x86 >= 1, x151 >= 1 -> x86'=x86-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x86 >= 1 -> x86'=x86-1, x87'=x87+1;
x87 >= 1, x151 >= 1 -> x87'=x87-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x87 >= 1 -> x87'=x87-1, x88'=x88+1;
x88 >= 1, x151 >= 1 -> x88'=x88-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x88 >= 1 -> x88'=x88-1, x89'=x89+1;
x89 >= 1, x151 >= 1 -> x89'=x89-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x89 >= 1 -> x89'=x89-1, x90'=x90+1;
x90 >= 1, x151 >= 1 -> x90'=x90-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x90 >= 1 -> x90'=x90-1, x91'=x91+1;
x91 >= 1, x151 >= 1 -> x91'=x91-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x91 >= 1 -> x91'=x91-1, x92'=x92+1;
x92 >= 1, x151 >= 1 -> x92'=x92-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x92 >= 1 -> x92'=x92-1, x93'=x93+1;
x93 >= 1, x151 >= 1 -> x93'=x93-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x93 >= 1 -> x93'=x93-1, x94'=x94+1;
x94 >= 1, x151 >= 1 -> x94'=x94-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x94 >= 1 -> x94'=x94-1, x95'=x95+1;
x95 >= 1, x151 >= 1 -> x95'=x95-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x95 >= 1 -> x95'=x95-1, x96'=x96+1;
x96 >= 1, x151 >= 1 -> x96'=x96-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x96 >= 1 -> x96'=x96-1, x97'=x97+1;
x97 >= 1, x151 >= 1 -> x97'=x97-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x97 >= 1 -> x97'=x97-1, x98'=x98+1;
x98 >= 1, x151 >= 1 -> x98'=x98-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x98 >= 1 -> x98'=x98-1, x99'=x99+1;
x99 >= 1, x151 >= 1 -> x99'=x99-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x99 >= 1 -> x99'=x99-1, x100'=x100+1;
x100 >= 1, x151 >= 1 -> x100'=x100-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x100 >= 1 -> x100'=x100-1, x101'=x101+1;
x101 >= 1, x151 >= 1 -> x101'=x101-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x101 >= 1 -> x101'=x101-1, x102'=x102+1;
x102 >= 1, x151 >= 1 -> x102'=x102-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x102 >= 1 -> x102'=x102-1, x103'=x103+1;
x103 >= 1, x151 >= 1 -> x103'=x103-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x103 >= 1 -> x103'=x103-1, x104'=x104+1;
x104 >= 1, x151 >= 1 -> x104'=x104-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x104 >= 1 -> x104'=x104-1, x105'=x105+1;
x105 >= 1, x151 >= 1 -> x105'=x105-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x105 >= 1 -> x105'=x105-1, x106'=x106+1;
x106 >= 1, x151 >= 1 -> x106'=x106-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x106 >= 1 -> x106'=x106-1, x107'=x107+1;
x107 >= 1, x151 >= 1 -> x107'=x107-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x107 >= 1 -> x107'=x107-1, x108'=x108+1;
x108 >= 1, x151 >= 1 -> x108'=x108-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x108 >= 1 -> x108'=x108-1, x109'=x109+1;
x109 >= 1, x151 >= 1 -> x109'=x109-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x109 >= 1 -> x109'=x109-1, x110'=x110+1;
x110 >= 1, x151 >= 1 -> x110'=x110-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x110 >= 1 -> x110'=x110-1, x111'=x111+1;
x111 >= 1, x151 >= 1 -> x111'=x111-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x111 >= 1 -> x111'=x111-1, x112'=x112+1;
x112 >= 1, x151 >= 1 -> x112'=x112-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x112 >= 1 -> x112'=x112-1, x113'=x113+1;
x113 >= 1, x151 >= 1 -> x113'=x113-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x113 >= 1 -> x113'=x113-1, x114'=x114+1;
x114 >= 1, x151 >= 1 -> x114'=x114-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x114 >= 1 -> x114'=x114-1, x115'=x115+1;
x115 >= 1, x151 >= 1 -> x115'=x115-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x115 >= 1 -> x115'=x115-1, x116'=x116+1;
x116 >= 1, x151 >= 1 -> x116'=x116-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x116 >= 1 -> x116'=x116-1, x117'=x117+1;
x117 >= 1, x151 >= 1 -> x117'=x117-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x117 >= 1 -> x117'=x117-1, x118'=x118+1;
x118 >= 1, x151 >= 1 -> x118'=x118-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x118 >= 1 -> x118'=x118-1, x119'=x119+1;
x119 >= 1, x151 >= 1 -> x119'=x119-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x119 >= 1 -> x119'=x119-1, x120'=x120+1;
x120 >= 1, x151 >= 1 -> x120'=x120-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x120 >= 1 -> x120'=x120-1, x121'=x121+1;
x121 >= 1, x151 >= 1 -> x121'=x121-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x121 >= 1 -> x121'=x121-1, x122'=x122+1;
x122 >= 1, x151 >= 1 -> x122'=x122-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x122 >= 1 -> x122'=x122-1, x123'=x123+1;
x123 >= 1, x151 >= 1 -> x123'=x123-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x123 >= 1 -> x123'=x123-1, x124'=x124+1;
x124 >= 1, x151 >= 1 -> x124'=x124-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x124 >= 1 -> x124'=x124-1, x125'=x125+1;
x125 >= 1, x151 >= 1 -> x125'=x125-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x125 >= 1 -> x125'=x125-1, x126'=x126+1;
x126 >= 1, x151 >= 1 -> x126'=x126-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x126 >= 1 -> x126'=x126-1, x127'=x127+1;
x127 >= 1, x151 >= 1 -> x127'=x127-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x127 >= 1 -> x127'=x127-1, x128'=x128+1;
x128 >= 1, x151 >= 1 -> x128'=x128-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x128 >= 1 -> x128'=x128-1, x129'=x129+1;
x129 >= 1, x151 >= 1 -> x129'=x129-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x129 >= 1 -> x129'=x129-1, x130'=x130+1;
x130 >= 1, x151 >= 1 -> x130'=x130-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x130 >= 1 -> x130'=x130-1, x131'=x131+1;
x131 >= 1, x151 >= 1 -> x131'=x131-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x131 >= 1 -> x131'=x131-1, x132'=x132+1;
x132 >= 1, x151 >= 1 -> x132'=x132-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x132 >= 1 -> x132'=x132-1, x133'=x133+1;
x133 >= 1, x151 >= 1 -> x133'=x133-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x133 >= 1 -> x133'=x133-1, x134'=x134+1;
x134 >= 1, x151 >= 1 -> x134'=x134-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x134 >= 1 -> x134'=x134-1, x135'=x135+1;
x135 >= 1, x151 >= 1 -> x135'=x135-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x135 >= 1 -> x135'=x135-1, x136'=x136+1;
x136 >= 1, x151 >= 1 -> x136'=x136-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x136 >= 1 -> x136'=x136-1, x137'=x137+1;
x137 >= 1, x151 >= 1 -> x137'=x137-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x137 >= 1 -> x137'=x137-1, x138'=x138+1;
x138 >= 1, x151 >= 1 -> x138'=x138-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x138 >= 1 -> x138'=x138-1, x139'=x139+1;
x139 >= 1, x151 >= 1 -> x139'=x139-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x139 >= 1 -> x139'=x139-1, x140'=x140+1;
x140 >= 1, x151 >= 1 -> x140'=x140-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x140 >= 1 -> x140'=x140-1, x141'=x141+1;
x141 >= 1, x151 >= 1 -> x141'=x141-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x141 >= 1 -> x141'=x141-1, x142'=x142+1;
x142 >= 1, x151 >= 1 -> x142'=x142-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x142 >= 1 -> x142'=x142-1, x143'=x143+1;
x143 >= 1, x151 >= 1 -> x143'=x143-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x143 >= 1 -> x143'=x143-1, x144'=x144+1;
x144 >= 1, x151 >= 1 -> x144'=x144-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x144 >= 1 -> x144'=x144-1, x145'=x145+1;
x145 >= 1, x151 >= 1 -> x145'=x145-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x145 >= 1 -> x145'=x145-1, x146'=x146+1;
x146 >= 1, x151 >= 1 -> x146'=x146-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x146 >= 1 -> x146'=x146-1, x147'=x147+1;
x147 >= 1, x151 >= 1 -> x147'=x147-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x147 >= 1 -> x147'=x147-1, x148'=x148+1;
x148 >= 1, x151 >= 1 -> x148'=x148-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x148 >= 1 -> x148'=x148-1, x149'=x149+1;
x149 >= 1, x151 >= 1 -> x149'=x149-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
x149 >= 1 -> x149'=x149-1, x150'=x150+1;
x150 >= 1, x151 >= 1 -> x150'=x150-1, x151'=x151-1, x0'=x0+1, x152'=x152+1;
init
x0 >= 1, x1 = 0, x2 = 0, x3 = 0, x4 = 0, x5 = 0, x6 = 0, x7 = 0, x8 = 0, x9 = 0, x10 = 0, x11 = 0, x12 = 0, x13 = 0, x14 = 0, x15 = 0, x16 = 0, x17 = 0, x18 = 0, x19 = 0, x20 = 0, x21 = 0, x22 = 0, x23 = 0, x24 = 0, x25 = 0, x26 = 0, x27 = 0, x28 = 0, x29 = 0, x30 = 0, x31 = 0, x32 = 0, x33 = 0, x34 = 0, x35 = 0, x36 = 0, x37 = 0, x38 = 0, x39 = 0, x40 = 0, x41 = 0, x42 = 0, x43 = 0, x44 = 0, x45 = 0, x46 = 0, x47 = 0, x48 = 0, x49 = 0, x50 = 0, x51 = 0, x52 = 0, x53 = 0, x54 = 0, x55 = 0, x56 = 0, x57 = 0, x58 = 0, x59 = 0, x60 = 0, x61 = 0, x62 = 0, x63 = 0, x64 = 0, x65 = 0, x66 = 0, x67 = 0, x68 = 0, x69 = 0, x70 = 0, x71 = 0, x72 = 0, x73 = 0, x74 = 0, x75 = 0, x76 = 0, x77 = 0, x78 = 0, x79 = 0, x80 = 0, x81 = 0, x82 = 0, x83 = 0, x84 = 0, x85 = 0, x86 = 0, x87 = 0, x88 = 0, x89 = 0, x90 = 0, x91 = 0, x92 = 0, x93 = 0, x94 = 0, x95 = 0, x96 = 0, x97 = 0, x98 = 0, x99 = 0, x100 = 0, x101 = 0, x102 = 0, x103 = 0, x104 = 0, x105 = 0, x106 = 0, x107 = 0, x108 = 0, x109 = 0, x110 = 0, x111 = 0, x112 = 0, x113 = 0, x114 = 0, x115 = 0, x116 = 0, x117 = 0, x118 = 0, x119 = 0, x120 = 0, x121 = 0, x122 = 0, x123 = 0, x124 = 0, x125 = 0, x126 = 0, x127 = 0, x128 = 0, x129 = 0, x130 = 0, x131 = 0, x132 = 0, x133 = 0, x134 = 0, x135 = 0, x136 = 0, x137 = 0, x138 = 0, x139 = 0, x140 = 0, x141 = 0, x142 = 0, x143 = 0, x144 = 0, x145 = 0, x146 = 0, x147 = 0, x148 = 0, x149 = 0, x150 = 0, x151 = 0, x152 = 1
target
x150 >= 2
vars
x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27
rules
x0 >= 1, x27 >= 1 -> x0'=x0-1, x27'=x27-1, x26'=x26+1, x1'=x1+1;
x1 >= 1, x27 >= 1 -> x1'=x1-1, x27'=x27-1, x26'=x26+1, x0'=x0+1;
x1 >= 1, x26 >= 1 -> x1'=x1-1, x26'=x26-1, x0'=x0+1, x27'=x27+1;
x1 >= 1 -> x1'=x1-1, x2'=x2+1;
x2 >= 1, x26 >= 1 -> x2'=x2-1, x26'=x26-1, x0'=x0+1, x27'=x27+1;
x2 >= 1 -> x2'=x2-1, x3'=x3+1;
x3 >= 1, x26 >= 1 -> x3'=x3-1, x26'=x26-1, x0'=x0+1, x27'=x27+1;
x3 >= 1 -> x3'=x3-1, x4'=x4+1;
x4 >= 1, x26 >= 1 -> x4'=x4-1, x26'=x26-1, x0'=x0+1, x27'=x27+1;
x4 >= 1 -> x4'=x4-1, x5'=x5+1;
x5 >= 1, x26 >= 1 -> x5'=x5-1, x26'=x26-1, x0'=x0+1, x27'=x27+1;
x5 >= 1 -> x5'=x5-1, x6'=x6+1;
x6 >= 1, x26 >= 1 -> x6'=x6-1, x26'=x26-1, x0'=x0+1, x27'=x27+1;
x6 >= 1 -> x6'=x6-1, x7'=x7+1;
x7 >= 1, x26 >= 1 -> x7'=x7-1, x26'=x26-1, x0'=x0+1, x27'=x27+1;
x7 >= 1 -> x7'=x7-1, x8'=x8+1;
x8 >= 1, x26 >= 1 -> x8'=x8-1, x26'=x26-1, x0'=x0+1, x27'=x27+1;
x8 >= 1 -> x8'=x8-1, x9'=x9+1;
x9 >= 1, x26 >= 1 -> x9'=x9-1, x26'=x26-1, x0'=x0+1, x27'=x27+1;
x9 >= 1 -> x9'=x9-1, x10'=x10+1;
x10 >= 1, x26 >= 1 -> x10'=x10-1, x26'=x26-1, x0'=x0+1, x27'=x27+1;
x10 >= 1 -> x10'=x10-1, x11'=x11+1;
x11 >= 1, x26 >= 1 -> x11'=x11-1, x26'=x26-1, x0'=x0+1, x27'=x27+1;
x11 >= 1 -> x11'=x11-1, x12'=x12+1;
x12 >= 1, x26 >= 1 -> x12'=x12-1, x26'=x26-1, x0'=x0+1, x27'=x27+1;
x12 >= 1 -> x12'=x12-1, x13'=x13+1;
x13 >= 1, x26 >= 1 -> x13'=x13-1, x26'=x26-1, x0'=x0+1, x27'=x27+1;
x13 >= 1 -> x13'=x13-1, x14'=x14+1;
x14 >= 1, x26 >= 1 -> x14'=x14-1, x26'=x26-1, x0'=x0+1, x27'=x27+1;
x14 >= 1 -> x14'=x14-1, x15'=x15+1;
x15 >= 1, x26 >= 1 -> x15'=x15-1, x26'=x26-1, x0'=x0+1, x27'=x27+1;
x15 >= 1 -> x15'=x15-1, x16'=x16+1;
x16 >= 1, x26 >= 1 -> x16'=x16-1, x26'=x26-1, x0'=x0+1, x27'=x27+1;
x16 >= 1 -> x16'=x16-1, x17'=x17+1;
x17 >= 1, x26 >= 1 -> x17'=x17-1, x26'=x26-1, x0'=x0+1, x27'=x27+1;
x17 >= 1 -> x17'=x17-1, x18'=x18+1;
x18 >= 1, x26 >= 1 -> x18'=x18-1, x26'=x26-1, x0'=x0+1, x27'=x27+1;
x18 >= 1 -> x18'=x18-1, x19'=x19+1;
x19 >= 1, x26 >= 1 -> x19'=x19-1, x26'=x26-1, x0'=x0+1, x27'=x27+1;
x19 >= 1 -> x19'=x19-1, x20'=x20+1;
x20 >= 1, x26 >= 1 -> x20'=x20-1, x26'=x26-1, x0'=x0+1, x27'=x27+1;
x20 >= 1 -> x20'=x20-1, x21'=x21+1;
x21 >= 1, x26 >= 1 -> x21'=x21-1, x26'=x26-1, x0'=x0+1, x27'=x27+1;
x21 >= 1 -> x21'=x21-1, x22'=x22+1;
x22 >= 1, x26 >= 1 -> x22'=x22-1, x26'=x26-1, x0'=x0+1, x27'=x27+1;
x22 >= 1 -> x22'=x22-1, x23'=x23+1;
x23 >= 1, x26 >= 1 -> x23'=x23-1, x26'=x26-1, x0'=x0+1, x27'=x27+1;
x23 >= 1 -> x23'=x23-1, x24'=x24+1;
x24 >= 1, x26 >= 1 -> x24'=x24-1, x26'=x26-1, x0'=x0+1, x27'=x27+1;
x24 >= 1 -> x24'=x24-1, x25'=x25+1;
x25 >= 1, x26 >= 1 -> x25'=x25-1, x26'=x26-1, x0'=x0+1, x27'=x27+1;
init
x0 >= 1, x1 = 0, x2 = 0, x3 = 0, x4 = 0, x5 = 0, x6 = 0, x7 = 0, x8 = 0, x9 = 0, x10 = 0, x11 = 0, x12 = 0, x13 = 0, x14 = 0, x15 = 0, x16 = 0, x17 = 0, x18 = 0, x19 = 0, x20 = 0, x21 = 0, x22 = 0, x23 = 0, x24 = 0, x25 = 0, x26 = 0, x27 = 1