aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNathanael Sensfelder <SpamShield0@MultiAgentSystems.org>2017-07-31 10:37:34 +0200
committerNathanael Sensfelder <SpamShield0@MultiAgentSystems.org>2017-07-31 10:37:34 +0200
commit98f12eaabfd4bdc04f60fdbfe7fec69bdc0eea37 (patch)
treee9b0fe84c17651bf4dd24de7316afcac967657f5
parent06c523d1692aae6fffcff2d0e617994d4b04bc55 (diff)
downloadtabellion-skol_only_the_solution.zip
tabellion-skol_only_the_solution.tar.bz2
Tagged variables are now the only skolemized vars.skol_only_the_solution
-rw-r--r--instr-to-kodkod/Makefile4
-rw-r--r--instr-to-kodkod/src/Main.java34
-rw-r--r--instr-to-kodkod/src/VHDLModel.java5
-rw-r--r--instr-to-kodkod/src/VHDLProperty.java4
-rw-r--r--instr-to-kodkod/src/VariableManager.java72
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);
+ }
+ }
}