Commit 5b9d9ef0 authored by Christian Müller's avatar Christian Müller
Browse files

add tests/metrics

parent 19d48092
......@@ -2,6 +2,19 @@
shopt -s nullglob
echo "Gobbling up metrics"
rm -f results/allmetrics.metrics
touch results/allmetrics.metrics
for FILE in results/*/*.metrics
echo "${FILE}:" >> results/allmetrics.metrics
cat ${FILE} >> results/allmetrics.metrics
echo -e "\n\n" >> results/allmetrics.metrics
for FILE in results/*/*.png
echo "Deleting ${FILE}"
......@@ -76,6 +76,15 @@ class InvariantCausalFilesTest extends FlatSpec {
assert(!checkSafeCausal(name, inv))
it should "fail to prove conference_linear with elim" in {
val name = "nonomitting/conference_linear"
val xt = Var("xt","X")
val yt = Var("yt","X")
val pt = Var("pt","P")
val inv = Forall(List(xt, pt, yt), genEq("Comm", List(xt, yt, pt)))
assert(!checkSafeCausalElim(name, inv))
it should "fail to prove nonomitting/conference" in {
val name = "nonomitting/conference"
val xt = Var("xat","X")
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