added two piece tests and test.sh script

diff --git a/modelchecker/main.c b/modelchecker/main.c
index fd37c23..7cc1070 100644 (file)
--- a/modelchecker/main.c
+++ b/modelchecker/main.c
@@ -68,7 +68,6 @@ void solve(FILE *inputstream)
        while(new != old){
                old = new;
                ERRPRINT("Iteration %d\n", iteration++);
-               ERRPRINT("Satcount: %f\n", sylvan_satcount(old, init->vars.varset));
         trans_t *t = rls->rell;
 
         while (t != NULL){
@@ -91,6 +90,7 @@ void solve(FILE *inputstream)
             t = t->next_rel;
         }
        }
+       ERRPRINT("Satcount: %f\n", sylvan_satcount(old, init->vars.varset));
                //sylvan_printdot_nc(old);
        //switch(strat){
        //      case COORD:

diff --git a/modelchecker/test.sh b/modelchecker/test.sh
new file mode 100755 (executable)
index 0000000..205c472
--- /dev/null
+++ b/modelchecker/test.sh
@@ -0,0 +1,15 @@
+#!/bin/bash
+
+for testscreen in tests/*; do
+       NUM="$(basename "$(echo $testscreen | cut -d'.' -f1)")"
+       OUT="$(./main "$testscreen" 2>&1| grep -Po "(?<=Satcount: )\d+(?=\.)")"
+       echo "Output: $OUT"
+       if [ "$NUM" -ne "$OUT" ]; then
+               echo "$testscreen failed"
+               echo "Expected: $NUM"
+               echo "Got: $OUT"
+               cat "$testscreen"
+       else
+               echo "$testscreen passed"
+       fi
+done

diff --git a/modelchecker/tests/1.a b/modelchecker/tests/1.a
new file mode 100644 (file)
index 0000000..59c227c
--- /dev/null
+++ b/modelchecker/tests/1.a
@@ -0,0 +1 @@
+@

diff --git a/modelchecker/tests/1.ae b/modelchecker/tests/1.ae
new file mode 100644 (file)
index 0000000..4092a4b
--- /dev/null
+++ b/modelchecker/tests/1.ae
@@ -0,0 +1,2 @@
+$
+@

diff --git a/modelchecker/tests/1.af b/modelchecker/tests/1.af
new file mode 100644 (file)
index 0000000..0616932
--- /dev/null
+++ b/modelchecker/tests/1.af
@@ -0,0 +1,2 @@
++
+$

diff --git a/modelchecker/tests/1.ag b/modelchecker/tests/1.ag
new file mode 100644 (file)
index 0000000..32c2eda
--- /dev/null
+++ b/modelchecker/tests/1.ag
@@ -0,0 +1,2 @@
+*
+@

diff --git a/modelchecker/tests/1.ah b/modelchecker/tests/1.ah
new file mode 100644 (file)
index 0000000..efebaa7
--- /dev/null
+++ b/modelchecker/tests/1.ah
@@ -0,0 +1,2 @@
++
+*

diff --git a/modelchecker/tests/1.b b/modelchecker/tests/1.b
new file mode 100644 (file)
index 0000000..fd38861
--- /dev/null
+++ b/modelchecker/tests/1.b
@@ -0,0 +1 @@
++

diff --git a/modelchecker/tests/1.g b/modelchecker/tests/1.g
new file mode 100644 (file)
index 0000000..17f5205
--- /dev/null
+++ b/modelchecker/tests/1.g
@@ -0,0 +1 @@
+@$

diff --git a/modelchecker/tests/1.h b/modelchecker/tests/1.h
new file mode 100644 (file)
index 0000000..0f36bec
--- /dev/null
+++ b/modelchecker/tests/1.h
@@ -0,0 +1 @@
++$

diff --git a/modelchecker/tests/1.i b/modelchecker/tests/1.i
new file mode 100644 (file)
index 0000000..90c254d
--- /dev/null
+++ b/modelchecker/tests/1.i
@@ -0,0 +1 @@
+@*

diff --git a/modelchecker/tests/1.j b/modelchecker/tests/1.j
new file mode 100644 (file)
index 0000000..1b4d99a
--- /dev/null
+++ b/modelchecker/tests/1.j
@@ -0,0 +1 @@
++*

diff --git a/modelchecker/tests/1.p b/modelchecker/tests/1.p
new file mode 100644 (file)
index 0000000..0616932
--- /dev/null
+++ b/modelchecker/tests/1.p
@@ -0,0 +1,2 @@
++
+$

diff --git a/modelchecker/tests/1.q b/modelchecker/tests/1.q
new file mode 100644 (file)
index 0000000..aba1deb
--- /dev/null
+++ b/modelchecker/tests/1.q
@@ -0,0 +1,2 @@
+@
+*

diff --git a/modelchecker/tests/1.r b/modelchecker/tests/1.r
new file mode 100644 (file)
index 0000000..efebaa7
--- /dev/null
+++ b/modelchecker/tests/1.r
@@ -0,0 +1,2 @@
++
+*

diff --git a/modelchecker/tests/1.w b/modelchecker/tests/1.w
new file mode 100644 (file)
index 0000000..8b13789
--- /dev/null
+++ b/modelchecker/tests/1.w
@@ -0,0 +1 @@
+

diff --git a/modelchecker/tests/1.x b/modelchecker/tests/1.x
new file mode 100644 (file)
index 0000000..0f36bec
--- /dev/null
+++ b/modelchecker/tests/1.x
@@ -0,0 +1 @@
++$

diff --git a/modelchecker/tests/1.y b/modelchecker/tests/1.y
new file mode 100644 (file)
index 0000000..0798a46
--- /dev/null
+++ b/modelchecker/tests/1.y
@@ -0,0 +1 @@
+*@

diff --git a/modelchecker/tests/1.z b/modelchecker/tests/1.z
new file mode 100644 (file)
index 0000000..1b4d99a
--- /dev/null
+++ b/modelchecker/tests/1.z
@@ -0,0 +1 @@
++*

diff --git a/modelchecker/tests/2.aa b/modelchecker/tests/2.aa
new file mode 100644 (file)
index 0000000..24ee4e8
--- /dev/null
+++ b/modelchecker/tests/2.aa
@@ -0,0 +1,2 @@
+ 
+@

diff --git a/modelchecker/tests/2.ab b/modelchecker/tests/2.ab
new file mode 100644 (file)
index 0000000..594628b
--- /dev/null
+++ b/modelchecker/tests/2.ab
@@ -0,0 +1,2 @@
+ 
++

diff --git a/modelchecker/tests/2.ac b/modelchecker/tests/2.ac
new file mode 100644 (file)
index 0000000..6be3ae1
--- /dev/null
+++ b/modelchecker/tests/2.ac
@@ -0,0 +1,2 @@
+.
+@

diff --git a/modelchecker/tests/2.ad b/modelchecker/tests/2.ad
new file mode 100644 (file)
index 0000000..8668798
--- /dev/null
+++ b/modelchecker/tests/2.ad
@@ -0,0 +1,2 @@
+.
++

diff --git a/modelchecker/tests/2.c b/modelchecker/tests/2.c
new file mode 100644 (file)
index 0000000..fe9a7f4
--- /dev/null
+++ b/modelchecker/tests/2.c
@@ -0,0 +1 @@
+@ 

diff --git a/modelchecker/tests/2.d b/modelchecker/tests/2.d
new file mode 100644 (file)
index 0000000..79f9ef5
--- /dev/null
+++ b/modelchecker/tests/2.d
@@ -0,0 +1 @@
++ 

diff --git a/modelchecker/tests/2.e b/modelchecker/tests/2.e
new file mode 100644 (file)
index 0000000..af5c276
--- /dev/null
+++ b/modelchecker/tests/2.e
@@ -0,0 +1 @@
+@.

diff --git a/modelchecker/tests/2.f b/modelchecker/tests/2.f
new file mode 100644 (file)
index 0000000..e5ef257
--- /dev/null
+++ b/modelchecker/tests/2.f
@@ -0,0 +1 @@
++.

diff --git a/modelchecker/tests/2.k b/modelchecker/tests/2.k
new file mode 100644 (file)
index 0000000..f42801b
--- /dev/null
+++ b/modelchecker/tests/2.k
@@ -0,0 +1,2 @@
+@
+ 

diff --git a/modelchecker/tests/2.l b/modelchecker/tests/2.l
new file mode 100644 (file)
index 0000000..0debfd0
--- /dev/null
+++ b/modelchecker/tests/2.l
@@ -0,0 +1,2 @@
++
+ 

diff --git a/modelchecker/tests/2.m b/modelchecker/tests/2.m
new file mode 100644 (file)
index 0000000..a381e1a
--- /dev/null
+++ b/modelchecker/tests/2.m
@@ -0,0 +1,2 @@
+@
+.

diff --git a/modelchecker/tests/2.n b/modelchecker/tests/2.n
new file mode 100644 (file)
index 0000000..f3e10c1
--- /dev/null
+++ b/modelchecker/tests/2.n
@@ -0,0 +1,2 @@
++
+.

diff --git a/modelchecker/tests/2.s b/modelchecker/tests/2.s
new file mode 100644 (file)
index 0000000..d575886
--- /dev/null
+++ b/modelchecker/tests/2.s
@@ -0,0 +1 @@
+ @

diff --git a/modelchecker/tests/2.t b/modelchecker/tests/2.t
new file mode 100644 (file)
index 0000000..8f4b4db
--- /dev/null
+++ b/modelchecker/tests/2.t
@@ -0,0 +1 @@
+ +

diff --git a/modelchecker/tests/2.u b/modelchecker/tests/2.u
new file mode 100644 (file)
index 0000000..694e87c
--- /dev/null
+++ b/modelchecker/tests/2.u
@@ -0,0 +1 @@
+.@

diff --git a/modelchecker/tests/2.v b/modelchecker/tests/2.v
new file mode 100644 (file)
index 0000000..b18168c
--- /dev/null
+++ b/modelchecker/tests/2.v
@@ -0,0 +1 @@
+.+

diff --git a/modelchecker/toy.screen b/modelchecker/toy.screen
deleted file mode 100644 (file)
index 87d52be..0000000
--- a/modelchecker/toy.screen
+++ /dev/null
@@ -1 +0,0 @@
-@ $