From 4942adb7022c95c0d2123b49601991e2a9d283ed Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Mon, 11 Apr 2016 02:43:58 +0200
Subject: [PATCH] Add graph subcommand to coalg
---
src/coalg/coalg.ml | 14 ++++++++++----
1 file changed, 10 insertions(+), 4 deletions(-)
diff --git a/src/coalg/coalg.ml b/src/coalg/coalg.ml
index f490b22..c87a7b1 100644
--- a/src/coalg/coalg.ml
+++ b/src/coalg/coalg.ml
@@ -167,6 +167,13 @@ let choiceNNF () =
done
with End_of_file -> ()
+let choiceGraph () =
+ choiceSat ();
+ print_endline "digraph reasonerstate {";
+ CM.graphIterCores (fun core -> print_endline (CM.coreToDot core));
+ CM.graphIterStates (fun state -> print_endline (CM.stateToDot state));
+ print_endline "}"
+
let choiceVerify () =
try
while true do
@@ -177,7 +184,7 @@ let choiceVerify () =
incr counter;
print_string ("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");
flush stdout;
- CoAlgFormula.verifyFormula f;
+ CoAlgFormula.verifyFormula f;
else ()
done
with End_of_file -> ()
@@ -213,7 +220,6 @@ let _ =
| "prov" -> choiceProvable ()
| "print" -> choicePrint ()
| "nnf" -> choiceNNF ()
- | "verify" -> choiceVerify ()
+ | "verify" -> choiceVerify ()
+ | "graph" -> choiceGraph ()
| _ -> printUsage ()
-
-
--
GitLab