diff --git a/tests/python/dca.test b/tests/python/dca.test index 894988951..f376656b6 100755 --- a/tests/python/dca.test +++ b/tests/python/dca.test @@ -23,7 +23,10 @@ set -e # Skip this test if ltl2dstar is not installed. (ltl2dstar --version) || exit 77 -cat >ba_formulas << 'EOF' +DIR=dca.dir +mkdir -p $DIR + +cat >$DIR/ba_formulas << 'EOF' FG((Xc & XXa) <-> !(b xor (c M b))) F!FGFb XF(b & Ga) @@ -40,7 +43,7 @@ XF((!c R a) W !Fb) (!a <-> !(c <-> Gb)) M 1 ((0 R a) M c) M ((b xor Fb) M F(b -> a)) EOF -cat >dsa_formulas <<'EOF' +cat >$DIR/dsa_formulas <<'EOF' (!b U b) U X(!a -> Fb) 1 U (a xor b) X(!(!b | (a M b)) -> XXa) @@ -48,11 +51,11 @@ X(!(!b | (a M b)) -> XXa) F(XF!a & (Fb U !a)) EOF while read ba_f; do - $srcdir/../run "$srcdir/dca.py" "$ba_f" > ba + ../run "$srcdir/dca.py" "$ba_f" > ba while read dsa_f; do ltldo -f "$dsa_f" "ltl2dstar --automata=streett\ - --ltl2nba=spin:ltl2tgba@-Ds" -H | autfilt --product=ba > input.hoa - autfilt --dca input.hoa > res.hoa - autfilt input.hoa --equivalent-to res.hoa - done $DIR/input.hoa + autfilt --dca $DIR/input.hoa > $DIR/res.hoa + autfilt $DIR/input.hoa --equivalent-to $DIR/res.hoa + done <$DIR/dsa_formulas +done <$DIR/ba_formulas