From 9631d5b75ce60fef7f1eebbdd95ebe5d1e8bc064 Mon Sep 17 00:00:00 2001
From: Kristin Braun <kristin.braun@fau.de>
Date: Sat, 18 Mar 2017 12:13:53 +0100
Subject: [PATCH] added nom2fix method
---
src/coalg/coalg.ml | 17 ++++++++++++++++-
1 file changed, 16 insertions(+), 1 deletion(-)
diff --git a/src/coalg/coalg.ml b/src/coalg/coalg.ml
index 30f4ec3..d04436e 100644
--- a/src/coalg/coalg.ml
+++ b/src/coalg/coalg.ml
@@ -46,7 +46,7 @@ let _ =
let printUsage () =
print_endline "Usage: \"alc <task> <functor> [<flags>]\" where";
- print_endline " <task> in { sat print verify nnf prov (is »not.(sat ¬f)«) }";
+ print_endline " <task> in { sat print verify nnf prov (is »not.(sat ¬f)«) nom2fix }";
print_endline " <functor> in { MultiModalK (or equivalently K)";
print_endline " MultiModalKD (or equivalently KD)";
print_endline " Monotone";
@@ -154,6 +154,20 @@ let choicePrint () =
done
with End_of_file -> ()
+let choiceNom2fix () =
+ try
+ while true do
+ let input = read_line () in
+ if not (GenAndComp.isEmptyString input) then
+ let f = CoAlgFormula.importFormula input in
+ let str = CoAlgFormula.exportFormula f in
+ incr counter;
+ print_string("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");
+ flush stdout;
+ else ()
+ done
+ with End_of_file -> ()
+
let choiceNNF () =
try
while true do
@@ -223,4 +237,5 @@ let _ =
| "nnf" -> choiceNNF ()
| "verify" -> choiceVerify ()
| "graph" -> choiceGraph ()
+ | "nom2fix" -> choiceNom2fix()
| _ -> printUsage ()
--
GitLab