Commit cc93a6d6 authored by martinez's avatar martinez
Browse files

* src/ltltest/reduccmp.test: Wrong test are removed.

parent c769f747
2004-06-17 Thomas Martinez <martinez@src.lip6.fr>
* src/ltltest/reduccmp.test: Wrong test are removed.
2004-06-17 Thomas Martinez <martinez@src.lip6.fr>
* src/tgbatest/spotlbtt.test: We don't check the post-reduction
......
......@@ -36,13 +36,13 @@ run 0 ./reduccmp 'a | (a U b)' 'a | (a U b)'
# Syntactic reduction
run 0 ./reduccmp 'a & (!b R !a)' 'false'
run 0 ./reduccmp '(!b R !a) & a' 'false'
run 0 ./reduccmp '(!b R !a) | a' 'true'
run 0 ./reduccmp 'a | (!b R !a)' 'true'
#run 0 ./reduccmp '(!b R !a) | a' 'true'
#run 0 ./reduccmp 'a | (!b R !a)' 'true'
run 0 ./reduccmp 'a & (!b R !a) & c' 'false'
run 0 ./reduccmp 'c & (!b R !a) & a' 'false'
run 0 ./reduccmp 'a | (!b R !a) | c' 'true'
run 0 ./reduccmp 'c | (!b R !a) | a' 'true'
#run 0 ./reduccmp 'a | (!b R !a) | c' 'true'
#run 0 ./reduccmp 'c | (!b R !a) | a' 'true'
run 0 ./reduccmp 'a & (b U a)' 'a'
run 0 ./reduccmp '(b U a) & a' 'a'
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment