From 84f47d6d66fda97c99ff0ec377b3754ebf33bf9b Mon Sep 17 00:00:00 2001 From: Mart Lubbers Date: Sun, 29 Nov 2015 11:04:59 +0100 Subject: [PATCH] try for 3b --- a2/src/3b.prv9 | 6 ++++++ a2/src/path.sh | 1 + 2 files changed, 7 insertions(+) create mode 100644 a2/src/3b.prv9 diff --git a/a2/src/3b.prv9 b/a2/src/3b.prv9 new file mode 100644 index 0000000..12c9aa4 --- /dev/null +++ b/a2/src/3b.prv9 @@ -0,0 +1,6 @@ +formulas(assumptions). +a(x, a(y, a(z, u))) -> a(y, a(z, a(x, u))). +end_of_list. +formulas(goals). +a(b, a(c, a(d, a(e, a(f, a(b, g)))))). +end_of_list. diff --git a/a2/src/path.sh b/a2/src/path.sh index d7dfea0..3603923 100644 --- a/a2/src/path.sh +++ b/a2/src/path.sh @@ -1,2 +1,3 @@ export PATH=$PATH:/home/mart/downloads/NuSMV-2.5.4/nusmv export PATH=$PATH:/home/mart/projects/NuSMV-2.6.0-Linux/bin +export PATH=$PATH:/home/mart/projects/LADR-2009-11A/bin -- 2.20.1