From: Mart Lubbers Date: Sun, 17 Apr 2016 16:40:43 +0000 (+0200) Subject: added two piece tests and test.sh script X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=b9f0343d3d3f07f8c1553bc44995a3c93c2de296;p=mc1516pa.git added two piece tests and test.sh script --- diff --git a/modelchecker/main.c b/modelchecker/main.c index fd37c23..7cc1070 100644 --- 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 index 87d52be..0000000 --- a/modelchecker/toy.screen +++ /dev/null @@ -1 +0,0 @@ -@ $