| summaryrefslogtreecommitdiff |
diff options
Diffstat (limited to 'cfg-to-paths/src/Main.java')
| -rw-r--r-- | cfg-to-paths/src/Main.java | 76 |
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()); + } } } |


