From 4c4531ea1abd2215f99f7c41e98c4d26f21089bb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <edu@thorsten-wissmann.de>
Date: Thu, 11 Feb 2016 17:19:44 +0100
Subject: [PATCH] CL: more test formulas
---
src/testsuite/cool-testsuite.ml | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/src/testsuite/cool-testsuite.ml b/src/testsuite/cool-testsuite.ml
index 35b4b3f..a6f312d 100644
--- a/src/testsuite/cool-testsuite.ml
+++ b/src/testsuite/cool-testsuite.ml
@@ -74,15 +74,19 @@ let cl_testcases : testcase_section =
; sat "[{1}] C & <{ 2 }> ~C"
; unsat "[{1}] C & <{ 1 2 }> ~C"
; sat "<{ 1 2 }> C & <{ 1 2 }> ~C"
+ ; sat "~([{ }] ~ phi <=> ~ [{1 2}] phi)"
; unsat "<{ 1 2 }> C & [{ 1 2 }] ~C"
; unsat "<{ 1 2 3 4 5 }> C & <{ 1 2 3 4 5 }> ~C"
; sat "([{1 3}] C) & ([{ 2 3 }] ~C )"
+ ; unsat "[{1}](p3 | ~p5) & ([{1}](p3 | p5) | [{1 2}](p1 | p3)) & ~[{1}](p5 | ~p4) & ([{}](~(p1 | ~p2)) | [{}](~(p1 | ~p4))) & [{}](~(p3 | ~p4)) & (~[{1}](p1 | ~p2) | ~[{1}](p1 | ~p5))"
+ ; sat "[{1}](p3 | ~p5) & ([{1}](p3 | p5) | [{1 2}](p1 | p3)) & ~[{1}](p5 | ~p4) & (~[{1 2 }]((p1 | ~p2)) | ~[{1 2}]((p1 | ~p4))) & ~[{1 2}]((p3 | ~p4)) & (~[{1}](p1 | ~p2) | ~[{1}](p1 | ~p5))"
]
let cl_testcases_2agents : testcase_section =
use_functor "CL" (fun () -> CoolUtils.cl_set_agents [|1;2|])
[ unsat "[{1}] C & [{ 2 }] ~C"
; unsat "<{ 1 2 }> C & <{ 1 2 }> ~C"
+ ; unsat "~([{ }] ~ phi <=> ~ [{1 2}] phi)"
; unsat "[{1}](p3 | ~p5) & ([{1}](p3 | p5) | [{1 2}](p1 | p3)) & ~[{1}](p5 | ~p4) & ([{}](~(p1 | ~p2)) | [{}](~(p1 | ~p4))) & [{}](~(p3 | ~p4)) & (~[{1}](p1 | ~p2) | ~[{1}](p1 | ~p5))"
; unsat "[{1}](p3 | ~p5) & ([{1}](p3 | p5) | [{1 2}](p1 | p3)) & ~[{1}](p5 | ~p4) & (~[{1 2 }]((p1 | ~p2)) | ~[{1 2}]((p1 | ~p4))) & ~[{1 2}]((p3 | ~p4)) & (~[{1}](p1 | ~p2) | ~[{1}](p1 | ~p5))"
]
--
GitLab