| summaryrefslogtreecommitdiff |
diff options
Diffstat (limited to 'instr-to-kodkod/src')
| -rw-r--r-- | instr-to-kodkod/src/Main.java | 108 | ||||
| -rw-r--r-- | instr-to-kodkod/src/Parameters.java | 79 | ||||
| -rw-r--r-- | instr-to-kodkod/src/StringManager.java | 11 | ||||
| -rw-r--r-- | instr-to-kodkod/src/VHDLPredicate.java | 5 | ||||
| -rw-r--r-- | instr-to-kodkod/src/VHDLType.java | 5 | ||||
| -rw-r--r-- | instr-to-kodkod/src/VariableManager.java | 37 |
6 files changed, 196 insertions, 49 deletions
diff --git a/instr-to-kodkod/src/Main.java b/instr-to-kodkod/src/Main.java index d6528cd..6a2445b 100644 --- a/instr-to-kodkod/src/Main.java +++ b/instr-to-kodkod/src/Main.java @@ -1,4 +1,7 @@ +import java.io.BufferedWriter; +import java.io.File; import java.io.FileNotFoundException; +import java.io.FileWriter; import java.io.IOException; import java.util.Iterator; @@ -20,6 +23,11 @@ public class Main private static VariableManager VARIABLE_MANAGER; private static StringManager STRING_MANAGER; + public static Parameters get_parameters () + { + return PARAMETERS; + } + public static VHDLModel get_model () { return MODEL; @@ -41,7 +49,10 @@ public class Main { try { - System.out.println("Loading level file \"" + lvl + "\"..."); + if (PARAMETERS.be_verbose()) + { + System.out.println("Loading level file \"" + lvl + "\"..."); + } VHDLLevel.add_to_model(MODEL, lvl); } @@ -71,12 +82,15 @@ public class Main try { - System.out.println - ( - "Loading property file \"" - + PARAMETERS.get_property_file() - + "\"..." - ); + if (PARAMETERS.be_verbose()) + { + System.out.println + ( + "Loading property file \"" + + PARAMETERS.get_property_file() + + "\"..." + ); + } return pro.generate_base_formula(); } @@ -100,7 +114,10 @@ public class Main { try { - System.out.println("Loading model file \"" + mod + "\"..."); + if (PARAMETERS.be_verbose()) + { + System.out.println("Loading model file \"" + mod + "\"..."); + } MODEL.parse_file(mod); } @@ -219,6 +236,29 @@ public class Main return true; } + private static BufferedWriter get_output_file (final String filename) + { + try + { + return new BufferedWriter(new FileWriter(new File(filename))); + } + catch (final Exception e) + { + System.err.println + ( + "[F] Could not create/open output file \"" + + filename + + "\":" + ); + + e.printStackTrace(); + + System.exit(-1); + } + + return null; + } + public static void main (final String... args) { /* @@ -238,6 +278,7 @@ public class Main final Iterator<Solution> solutions; final Solver solver; final Formula property; + final BufferedWriter solution_output; PARAMETERS = new Parameters(args); @@ -246,7 +287,14 @@ public class Main return; } - VARIABLE_MANAGER = new VariableManager(PARAMETERS.get_variables_prefix()); + solution_output = get_output_file(PARAMETERS.get_output_file()); + + if (solution_output == null) + { + return; + } + + VARIABLE_MANAGER = new VariableManager(); MODEL = new VHDLModel(); @@ -271,7 +319,7 @@ public class Main { return; } - else + else if (PARAMETERS.be_verbose()) { System.out.println ( @@ -320,8 +368,46 @@ public class Main if (sol.sat()) { - VARIABLE_MANAGER.print_solution(sol.instance().relationTuples()); + try + { + VARIABLE_MANAGER.print_solution + ( + sol.instance().relationTuples(), + solution_output + ); + } + catch (final IOException e) + { + System.err.println + ( + "[F] Unable to write solution to file \"" + + PARAMETERS.get_output_file() + + "\":" + ); + + e.printStackTrace(); + + System.exit(-1); + } } } + + try + { + solution_output.close(); + } + catch (final IOException e) + { + System.err.println + ( + "[F] Unable to properly close solution file \"" + + PARAMETERS.get_output_file() + + "\":" + ); + + e.printStackTrace(); + + System.exit(-1); + } } } diff --git a/instr-to-kodkod/src/Parameters.java b/instr-to-kodkod/src/Parameters.java index d3bc0f1..7c80474 100644 --- a/instr-to-kodkod/src/Parameters.java +++ b/instr-to-kodkod/src/Parameters.java @@ -7,7 +7,8 @@ public class Parameters private final List<String> model_files; private final List<String> map_files; private final String property_file; - private final String var_prefix; + private final String output_file; + private final boolean be_verbose; private final boolean are_valid; @@ -17,12 +18,14 @@ public class Parameters ( "Instr-to-kodkod\n" + "USAGE:\n" - + "\tjava Main <VAR_PREFIX> <FILES>+\n" + + "\tjava Main <OUTPUT_FILE> <FILES|OPTIONS>+\n" + "PARAMETERS:\n" - + "\t- <VAR_PREFIX>\tPrefix for anonymous variables (e.g. \"_anon_\").\n" + + "\t- <OUTPUT_FILE>\tFile to write the solutions in.\n" + "\t- <FILES>\tList of files to be loaded.\n" + + "OPTIONS:\n" + + "\t- -v|--verbose\tPrint informative messages to STDOUT.\n" + "NOTES:\n" - + "\t- One, single, property file MUST be in <FILES>.\n" + + "\t- Exactly one property file must be in <FILES>.\n" + "\t- Property files have a \".pro\" extension.\n" + "\t- Model files have a \".mod\" extension.\n" + "\t- Level files have a \".lvl\" extension.\n" @@ -31,23 +34,26 @@ public class Parameters ); } - public Parameters (String... args) + public Parameters (final String... args) { - boolean has_pro_file, has_error; + boolean has_pro_file, has_error, should_be_verbose; String prop_file; level_files = new ArrayList<String>(); model_files = new ArrayList<String>(); map_files = new ArrayList<String>(); + should_be_verbose = false; + if (args.length < 2) { print_usage(); property_file = new String(); - var_prefix = new String(); + output_file = new String(); are_valid = false; + be_verbose = false; return; } @@ -55,7 +61,48 @@ public class Parameters has_pro_file = false; has_error = false; - var_prefix = args[0]; + output_file = args[0]; + + if + ( + (output_file.equals("-v") || output_file.equals("--verbose")) + /* || ... */ + ) + { + print_usage(); + + System.err.println + ( + "[F] An option was found in lieu of the output file." + ); + + System.exit(-1); + } + + if + ( + output_file.endsWith(".lvl") + || output_file.endsWith(".mod") + || output_file.endsWith(".map") + || output_file.endsWith(".pro") + ) + { + print_usage(); + + System.err.println + ( + "[F] The output file has an extension that could be used in an" + + " input file. It is most likely that you did not indicate an" + + " output file, meaning that one of the input files was about to" + + " be written over. So likely, in fact, that we'll abort here. The" + + " output file you indicated was \"" + + output_file + + "\"." + ); + + System.exit(-1); + } + prop_file = new String(); for (int i = 1; i < args.length; ++i) @@ -65,7 +112,7 @@ public class Parameters level_files.add(args[i]); } else if (args[i].endsWith(".mod")) - { + { model_files.add(args[i]); } else if (args[i].endsWith(".map")) @@ -93,6 +140,10 @@ public class Parameters prop_file = args[i]; } } + else if (output_file.equals("-v") || output_file.equals("--verbose")) + { + should_be_verbose = true; + } else { System.err.println @@ -115,6 +166,7 @@ public class Parameters has_error = true; } + be_verbose = should_be_verbose; are_valid = !has_error; } @@ -138,9 +190,14 @@ public class Parameters return property_file; } - public String get_variables_prefix () + public String get_output_file () + { + return output_file; + } + + public boolean be_verbose () { - return var_prefix; + return be_verbose; } public boolean are_valid () diff --git a/instr-to-kodkod/src/StringManager.java b/instr-to-kodkod/src/StringManager.java index c0a2fa4..247d8e3 100644 --- a/instr-to-kodkod/src/StringManager.java +++ b/instr-to-kodkod/src/StringManager.java @@ -41,17 +41,6 @@ public class StringManager TO_ID.put(str, id); } - else - { - System.out.println - ( - "[D] Using string \"" - + str - + "\" (id: " - + id - + ")" - ); - } return string_type.get_member_as_relation(id); } diff --git a/instr-to-kodkod/src/VHDLPredicate.java b/instr-to-kodkod/src/VHDLPredicate.java index 821a044..1b4d16d 100644 --- a/instr-to-kodkod/src/VHDLPredicate.java +++ b/instr-to-kodkod/src/VHDLPredicate.java @@ -71,7 +71,10 @@ public class VHDLPredicate is_used = true; - System.out.println("Enabling predicate: " + name); + if (Main.get_parameters().be_verbose()) + { + System.out.println("Enabling predicate: " + name); + } } return as_relation; diff --git a/instr-to-kodkod/src/VHDLType.java b/instr-to-kodkod/src/VHDLType.java index d8ae9ed..e38af5e 100644 --- a/instr-to-kodkod/src/VHDLType.java +++ b/instr-to-kodkod/src/VHDLType.java @@ -44,7 +44,10 @@ public class VHDLType { if (!is_used) { - System.out.println("Enabling type: " + name); + if (Main.get_parameters().be_verbose()) + { + System.out.println("Enabling type: " + name); + } is_used = true; } diff --git a/instr-to-kodkod/src/VariableManager.java b/instr-to-kodkod/src/VariableManager.java index cf7229e..249b183 100644 --- a/instr-to-kodkod/src/VariableManager.java +++ b/instr-to-kodkod/src/VariableManager.java @@ -1,3 +1,6 @@ +import java.io.BufferedWriter; +import java.io.IOException; + import java.util.HashMap; import java.util.Map; @@ -16,7 +19,7 @@ public class VariableManager private final Map<String, TaggedVariable> tagged_variables; private int next_id; - public VariableManager (final String var_prefix) + public VariableManager () { from_string = new HashMap<String, Expression>(); tagged_variables = new HashMap<String, TaggedVariable>(); @@ -43,8 +46,6 @@ public class VariableManager { final TaggedVariable tg; - System.out.println("[D] Skolemizing: " + var_name); - if (from_string.containsKey(var_name)) { throw @@ -149,25 +150,33 @@ public class VariableManager return result; } - public void print_solution (final Map<Relation, TupleSet> solution) + public void print_solution + ( + final Map<Relation, TupleSet> solution, + final BufferedWriter output + ) + throws IOException { - System.out.print("(solution"); + output.write("(solution"); for (final TaggedVariable tg: tagged_variables.values()) { - System.out.print("\n ("); - System.out.print(tg.name); - System.out.print(" "); - System.out.print + output.newLine(); + output.write(" ("); + output.write(tg.name); + output.write(" "); + output.write ( - solution.get(tg.as_relation).iterator().next().atom(0) + solution.get(tg.as_relation).iterator().next().atom(0).toString() ); - System.out.print(" "); - System.out.print(tg.tag); - System.out.print(")"); + output.write(" "); + output.write(tg.tag); + output.write(")"); } - System.out.println("\n)"); + output.newLine(); + output.write(")"); + output.newLine(); } private static class TaggedVariable |