From 64c8b8413db37494f118c7a2f50c186830fb64dc Mon Sep 17 00:00:00 2001 From: Nathanael Sensfelder Date: Tue, 18 Jul 2017 17:47:49 +0200 Subject: Starting to link parser with the program. But apparently I messed up some kodkod logic. --- instr-to-kodkod/src/Main.java | 13 ++++++++ instr-to-kodkod/src/Parameters.java | 13 ++++++-- instr-to-kodkod/src/VariableManager.java | 57 ++++++++++++++++++++++++++++++++ 3 files changed, 81 insertions(+), 2 deletions(-) create mode 100644 instr-to-kodkod/src/VariableManager.java (limited to 'instr-to-kodkod/src') diff --git a/instr-to-kodkod/src/Main.java b/instr-to-kodkod/src/Main.java index ba9ebaa..41b8ef8 100644 --- a/instr-to-kodkod/src/Main.java +++ b/instr-to-kodkod/src/Main.java @@ -10,6 +10,17 @@ public class Main { private static Parameters PARAMETERS; private static VHDLModel MODEL; + private static VariableManager VARIABLE_MANAGER; + + public static VHDLModel get_model () + { + return MODEL; + } + + public static VariableManager get_variable_manager () + { + return VARIABLE_MANAGER; + } private static Formula get_formula (final VHDLModel model) { @@ -49,6 +60,8 @@ public class Main return; } + VARIABLE_MANAGER = new VariableManager(PARAMETERS.get_variables_prefix()); + MODEL = new VHDLModel(); /* 1/ Load Levels (Types + predicates) */ diff --git a/instr-to-kodkod/src/Parameters.java b/instr-to-kodkod/src/Parameters.java index e9dc648..1face97 100644 --- a/instr-to-kodkod/src/Parameters.java +++ b/instr-to-kodkod/src/Parameters.java @@ -2,6 +2,7 @@ public class Parameters { private final String levels_dir; private final String model_file; + private final String var_prefix; private final boolean are_valid; public static void print_usage () @@ -10,10 +11,11 @@ public class Parameters ( "Instr-to-kodkod\n" + "USAGE:\n" - + "\tjava Main \n" + + "\tjava Main \n" + "PARAMETERS:\n" + "\t\tDirectory containing the level definitions.\n" + "\t\tInstruction file describing the model.\n" + + "\t\tPrefix for anonymous variables (e.g. \"_anon_\").\n" + "NOTES:\n" + "\tThe properties to be verified still have to be hand coded in the" + " source files (in Main.java)." @@ -22,18 +24,20 @@ public class Parameters public Parameters (String... args) { - if (args.length != 2) + if (args.length != 3) { print_usage(); levels_dir = new String(); model_file = new String(); + var_prefix = new String(); are_valid = false; } else { levels_dir = args[0]; model_file = args[1]; + var_prefix = args[2]; are_valid = true; } } @@ -48,6 +52,11 @@ public class Parameters return model_file; } + public String get_variables_prefix () + { + return var_prefix; + } + public boolean are_valid () { return are_valid; diff --git a/instr-to-kodkod/src/VariableManager.java b/instr-to-kodkod/src/VariableManager.java new file mode 100644 index 0000000..381a774 --- /dev/null +++ b/instr-to-kodkod/src/VariableManager.java @@ -0,0 +1,57 @@ +/* FIXME: finer imports. */ +import java.util.*; + +import kodkod.ast.*; + +public class VariableManager +{ + private final Map from_string; + private final Map tags; + private final String var_prefix; + private int next_id; + + public VariableManager (final String var_prefix) + { + from_string = new HashMap(); + tags = new HashMap(); + + this.var_prefix = var_prefix; + } + + private String generate_new_id () + { + final String result; + + result = var_prefix + next_id; + + next_id += 1; + + return result; + } + + public Variable get_variable (final String name) + { + Variable result; + + result = from_string.get(name); + + if (result == null) + { + result = Variable.unary(name); + + from_string.put(name, result); + } + + return result; + } + + public Variable generate_new_variable () + { + return get_variable(generate_new_id()); + } + + public void tag_variable (final String name, final String tag) + { + tags.put(name, tag); + } +} -- cgit v1.2.3-70-g09d2