From 9d530ce78b12f25a0b98007f79793f73549e2cfc Mon Sep 17 00:00:00 2001
From: Hans-Peter Deifel <hans-peter.deifel@fau.de>
Date: Tue, 10 Oct 2017 23:28:31 +0200
Subject: [PATCH] Add negation to generator for phi
---
gen.ml | 39 ++++++++++++++++++++++++++++++++-------
1 file changed, 32 insertions(+), 7 deletions(-)
diff --git a/gen.ml b/gen.ml
index d761943..ed618a6 100644
--- a/gen.ml
+++ b/gen.ml
@@ -23,6 +23,17 @@ let conjoin list = match list with
let box name = const_ax "" (VAR name)
+let psi n =
+ let inside i =
+ let not_qis =
+ List.map (fun j -> (NOT (AP (name "q" j))))
+ (List.filter (fun x -> x <> i) (iota n))
+ in
+ (const_and (AP (name "q" i)) (conjoin not_qis))
+ in
+
+ (NU("X",const_and (box "X") (disjoin (List.map inside (iota n)))))
+
let psi_neg n =
let inside i =
let qis =
@@ -105,7 +116,10 @@ let phi n =
(const_or (before_biimpl_neg n) (after_biimpl n))
(const_or (before_biimpl n) (after_biimpl_neg n)))
-
+let neg_phi n =
+ const_and (psi n)
+ (const_or (const_and (before_biimpl n) (after_biimpl_neg n))
+ (const_and (before_biimpl_neg n) (after_biimpl n)))
exception CTLException of string
@@ -222,10 +236,21 @@ let exportMLSolver f =
expML f;
Buffer.contents sb
+let print_usage () =
+ print_endline ("Usage: " ^ Sys.argv.(0) ^ " (pos|neg) (cool|mlsolver) n");
+ print_endline (" where n is the number of the formula to generate")
+
let () =
- let n = int_of_string Sys.argv.(2) in
- print_endline begin
- match Sys.argv.(1) with
- | "cool" -> (exportFormula (phi n))
- | "mlsolver" -> (exportMLSolver (phi n))
- end
+ if Array.length Sys.argv <> 4 then
+ print_usage ()
+ else
+ let n = int_of_string Sys.argv.(3) in
+ let f = match Sys.argv.(1) with
+ | "pos" -> phi
+ | "neg" -> neg_phi
+ | _ -> print_usage (); exit 1
+ in
+ match Sys.argv.(2) with
+ | "cool" -> print_endline (exportFormula (f n))
+ | "mlsolver" -> print_endline (exportMLSolver (f n))
+ | _ -> print_usage ()
--
GitLab