| summaryrefslogtreecommitdiff |
diff options
| -rw-r--r-- | instr-to-kodkod/Makefile | 4 | ||||
| -rw-r--r-- | instr-to-kodkod/src/Main.java | 34 | ||||
| -rw-r--r-- | instr-to-kodkod/src/VHDLModel.java | 5 | ||||
| -rw-r--r-- | instr-to-kodkod/src/VHDLProperty.java | 4 | ||||
| -rw-r--r-- | instr-to-kodkod/src/VariableManager.java | 72 |
5 files changed, 99 insertions, 20 deletions
diff --git a/instr-to-kodkod/Makefile b/instr-to-kodkod/Makefile index fa91a23..7232a6e 100644 --- a/instr-to-kodkod/Makefile +++ b/instr-to-kodkod/Makefile @@ -10,9 +10,9 @@ LEVEL_DIR = $(wildcard ../data/level/*.lvl) #PROPERTY_FILE = ../data/property/unread_waveforms.pro #PROPERTY_FILE = ../data/property/impossible_processes.pro #PROPERTY_FILE = ../data/property/incrementer.pro -#PROPERTY_FILE = ../data/property/combinational_processes.pro +PROPERTY_FILE = ../data/property/combinational_processes.pro #PROPERTY_FILE = ../data/property/likely_a_clock.pro -PROPERTY_FILE = ../data/property/cnes/CNE*.pro +#PROPERTY_FILE = ../data/property/cnes/CNE*.pro VAR_PREFIX = "_anon_" ## Executables ################################################################# diff --git a/instr-to-kodkod/src/Main.java b/instr-to-kodkod/src/Main.java index d8393bd..554fa17 100644 --- a/instr-to-kodkod/src/Main.java +++ b/instr-to-kodkod/src/Main.java @@ -222,10 +222,13 @@ public class Main /* * Order of operations: * 1/ Load Levels (Types + predicates) - * 2/ Load Properties (will change 'is_used()' on predicates) - * 3/ Generate complementary model according to used predicates. - * 4/ Load Model, but only for used predicates and types. - * 5/ Add all used types and predicates to the Universe. + * 2/ Load Mappings (string handling, some already have IDs). + * 3/ Load Property (will change 'is_used()' on predicates). + * 4/ Generate model according to the used predicates. + * 5/ Load Model, but only for used predicates and types. + * 6/ Add all used types and predicates to the Universe. + * 7/ Solve regular expressions. + * 8/ Add constraints linked to tagged variables. */ final Universe univ; final TupleFactory tf; @@ -259,8 +262,7 @@ public class Main return; } - /* 2/ Load Properties (will change 'is_used()' on predicates) */ - /* FIXME? Currently only one property, due to the 'is_used' */ + /* 3/ Load Properties (will change 'is_used()' on predicates) */ property = load_property(); if (property == null) @@ -276,27 +278,37 @@ public class Main ); } - /* 3/ Generate complementary model according to used predicates. */ - /* TODO */ + /* 4/ Generate model according to used predicates. */ + /* Done implicitly by step 5. - /* 4/ Load Model, but only for used predicates and types. */ + /* 5/ Load Model, but only for used predicates and types. */ if (!load_models()) { return; } - /* 5/ Add all types and used predicates to the Universe. */ + /* 6/ Add all types and used predicates to the Universe. */ univ = new Universe(MODEL.get_atoms()); tf = univ.factory(); bounds = new Bounds(univ); MODEL.add_to_bounds(bounds, tf); + VARIABLE_MANAGER.add_tagged_variables_to_bounds(bounds, tf); solver = new Solver(); + solver.options().setSkolemDepth(-1); solver.options().setSolver(SATFactory.DefaultSAT4J); solver.options().setReporter(new ConsoleReporter()); - solutions = solver.solveAll(property, bounds); + solutions = + solver.solveAll + ( + property.and + ( + VARIABLE_MANAGER.generate_tagged_variable_constraints() + ), + bounds + ); while (solutions.hasNext()) { diff --git a/instr-to-kodkod/src/VHDLModel.java b/instr-to-kodkod/src/VHDLModel.java index 170ce12..b1086f1 100644 --- a/instr-to-kodkod/src/VHDLModel.java +++ b/instr-to-kodkod/src/VHDLModel.java @@ -329,6 +329,11 @@ public class VHDLModel } } + public VHDLType get_type (final String name) + { + return types.get(name); + } + public Relation get_type_as_relation (final String name) { final VHDLType t; diff --git a/instr-to-kodkod/src/VHDLProperty.java b/instr-to-kodkod/src/VHDLProperty.java index ac88e6e..f74aae4 100644 --- a/instr-to-kodkod/src/VHDLProperty.java +++ b/instr-to-kodkod/src/VHDLProperty.java @@ -9,14 +9,10 @@ import org.antlr.v4.runtime.*; public class VHDLProperty { private final String filename; - private final List<Variable> tagged_variables; - private final List<VHDLType> tagged_variables_types; public VHDLProperty (final String filename) { this.filename = filename; - tagged_variables = new ArrayList<Variable>(); - tagged_variables_types = new ArrayList<VHDLType>(); } public Formula generate_base_formula () diff --git a/instr-to-kodkod/src/VariableManager.java b/instr-to-kodkod/src/VariableManager.java index eaa20d2..4753341 100644 --- a/instr-to-kodkod/src/VariableManager.java +++ b/instr-to-kodkod/src/VariableManager.java @@ -3,16 +3,18 @@ import java.util.*; import kodkod.ast.*; +import kodkod.instance.*; + public class VariableManager { private final Map<String, Expression> from_string; - private final Map<String, String> tags; + private final Map<String, TaggedVariable> tagged_variables; private int next_id; public VariableManager (final String var_prefix) { from_string = new HashMap<String, Expression>(); - tags = new HashMap<String, String>(); + tagged_variables = new HashMap<String, TaggedVariable>(); } private String generate_new_anonymous_variable_name () @@ -34,6 +36,8 @@ public class VariableManager ) throws Exception { + final TaggedVariable tg; + System.out.println("[D] Skolemizing: " + var_name); if (from_string.containsKey(var_name)) @@ -48,7 +52,10 @@ public class VariableManager ); } - from_string.put(var_name, Variable.unary(var_name)); + tg = new TaggedVariable(var_name, var_type, tag_name); + + from_string.put(var_name, tg.as_relation); + tagged_variables.put(var_name, tg); } public Variable add_variable (final String var_name) @@ -99,4 +106,63 @@ public class VariableManager { return Variable.unary(generate_new_anonymous_variable_name()); } + + public void add_tagged_variables_to_bounds + ( + final Bounds b, + final TupleFactory f + ) + { + for (final TaggedVariable tg: tagged_variables.values()) + { + b.bound + ( + tg.as_relation, + f.setOf(new Object[0]), + f.setOf + ( + Main.get_model().get_type + ( + tg.type + ).get_all_members_as_atoms().toArray() + ) + ); + } + } + + public Formula generate_tagged_variable_constraints () + { + Formula result; + + result = Formula.TRUE; + + for (final TaggedVariable tg: tagged_variables.values()) + { + result = result.and(tg.as_relation.one()); + } + + return result; + } + + private static class TaggedVariable + { + private final String name; + private final String type; + private final String tag; + private final Relation as_relation; + + private TaggedVariable + ( + final String name, + final String type, + final String tag + ) + { + this.name = name; + this.type = type; + this.tag = tag; + + as_relation = Relation.unary(name); + } + } } |