Working on a way to CTL over DAG in Kodkod.

1 files changed, 91 insertions, 0 deletions

diff --git a/cfg-to-paths/src/Main.java b/cfg-to-paths/src/Main.java
new file mode 100644
index 0000000..ec55450
--- /dev/null
+++ b/cfg-to-paths/src/Main.java
@@ -0,0 +1,91 @@
+/* FIXME: Finer imports */
+import kodkod.ast.*;
+
+import kodkod.engine.*;
+import kodkod.engine.config.*;
+import kodkod.engine.satlab.*;
+
+import kodkod.instance.*;
+public class Main
+{
+   private static Parameters PARAMETERS;
+
+   private static Formula get_formula (final VHDLModel model)
+   {
+      final Variable w;
+
+      w = Variable.unary("w");
+
+      return
+         w.join
+         (
+            model.get_predicate_as_relation("is_accessed_by")
+         ).no().forSome(w.oneOf(model.get_type_as_relation("waveform")));
+   }
+
+   public static void main (final String... args)
+   {
+      final VHDLModel model;
+
+      final Universe univ;
+      final TupleFactory tf;
+      final Bounds bounds;
+
+      final Solver solver;
+      final Solution sol;
+
+      PARAMETERS = new Parameters(args);
+
+      if (!PARAMETERS.are_valid())
+      {
+         return;
+      }
+
+      model = new VHDLModel();
+
+      try
+      {
+         VHDLLevel.add_to_model
+         (
+            model,
+            (
+               PARAMETERS.get_levels_directory()
+               + "/structural_level.data"
+            )
+         );
+      }
+      catch (final Exception e)
+      {
+         System.err.println("[E] Could not load structural level:");
+         e.printStackTrace();
+
+         return;
+      }
+
+      try
+      {
+         model.parse_file(PARAMETERS.get_model_file());
+      }
+      catch (final Exception e)
+      {
+         System.err.println("[E] Could not load instructions:");
+         e.printStackTrace();
+
+         return;
+      }
+
+      univ = new Universe(model.get_atoms());
+      tf = univ.factory();
+      bounds = new Bounds(univ);
+
+      model.add_to_bounds(bounds, tf);
+
+      solver = new Solver();
+      solver.options().setSolver(SATFactory.DefaultSAT4J);
+      solver.options().setReporter(new ConsoleReporter());
+
+      sol = solver.solve(get_formula(model), bounds);
+
+      System.out.println(sol);
+   }
+}