summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to 'cfg-to-paths/src/Main.java')
-rw-r--r--cfg-to-paths/src/Main.java76
1 files changed, 16 insertions, 60 deletions
diff --git a/cfg-to-paths/src/Main.java b/cfg-to-paths/src/Main.java
index ec55450..f81b22f 100644
--- a/cfg-to-paths/src/Main.java
+++ b/cfg-to-paths/src/Main.java
@@ -1,38 +1,14 @@
/* FIXME: Finer imports */
-import kodkod.ast.*;
+import java.util.*;
-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;
+ final Collection<Path> all_paths;
+ final Collection<List<Node>> all_subpaths;
PARAMETERS = new Parameters(args);
@@ -41,51 +17,31 @@ public class Main
return;
}
- model = new VHDLModel();
-
try
{
- VHDLLevel.add_to_model
- (
- model,
- (
- PARAMETERS.get_levels_directory()
- + "/structural_level.data"
- )
- );
+ ControlFlow.load_file(PARAMETERS.get_model_file());
}
catch (final Exception e)
{
- System.err.println("[E] Could not load structural level:");
- e.printStackTrace();
-
- return;
- }
+ System.err.println
+ (
+ "[E] Could not load model file \""
+ + PARAMETERS.get_model_file()
+ + "\":"
+ );
- 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);
+ all_paths = Path.get_all_paths_from(PARAMETERS.get_root_node());
- solver = new Solver();
- solver.options().setSolver(SATFactory.DefaultSAT4J);
- solver.options().setReporter(new ConsoleReporter());
+ all_subpaths = new ArrayList<List<Node>>();
- sol = solver.solve(get_formula(model), bounds);
-
- System.out.println(sol);
+ for (final Path p: all_paths)
+ {
+ all_subpaths.addAll(p.get_all_subpaths());
+ }
}
}