From ee9d405bc917be3f596ccd2ffd2d7ddc01687d31 Mon Sep 17 00:00:00 2001 From: Nathanael Sensfelder Date: Mon, 28 Aug 2017 16:27:12 +0200 Subject: Starts the Instance Calculator --- instance-calculator/Makefile | 69 +++++++++++++++++++++++++++ instance-calculator/src/.java_classpath | 1 + instance-calculator/src/VHDLArchitecture.java | 22 +++++++++ instance-calculator/src/VHDLComponent.java | 21 ++++++++ instance-calculator/src/VHDLEntity.java | 21 ++++++++ instance-calculator/src/VHDLProcess.java | 21 ++++++++ 6 files changed, 155 insertions(+) create mode 100644 instance-calculator/Makefile create mode 100644 instance-calculator/src/.java_classpath create mode 100644 instance-calculator/src/VHDLArchitecture.java create mode 100644 instance-calculator/src/VHDLComponent.java create mode 100644 instance-calculator/src/VHDLEntity.java create mode 100644 instance-calculator/src/VHDLProcess.java diff --git a/instance-calculator/Makefile b/instance-calculator/Makefile new file mode 100644 index 0000000..8da7891 --- /dev/null +++ b/instance-calculator/Makefile @@ -0,0 +1,69 @@ +## Parameters ################################################################## +#### Where to find the model +ifndef MODEL_DIR +MODEL_DIR = +endif + +#### Where to store the Instance model +ifndef INSTANCE_MODEL_DIR +INSTANCE_MODEL_DIR = +endif + +#### Binaries +###### JRE binary +ifndef JAVA +JAVA = java +endif + +###### JDK binary +ifndef JAVAC +JAVAC = javac +endif + +## Parameters Sanity Check ##################################################### +ifeq ($(strip $(MODEL_DIR)),) +$(error No MODEL_DIR defined as parameter.) +endif + +ifeq ($(strip $(INSTANCE_MODEL_DIR)),) +$(error No INSTANCE_MODEL_DIR defined as parameter.) +endif + +ifeq ($(strip $(JAVA)),) +$(error No Java executable defined as parameter.) +endif + +ifeq ($(strip $(JAVAC)),) +$(error No Java compiler defined as parameter.) +endif + +################################################################################ +CLASSPATH = "./src/" + +## Makefile Magic ############################################################## +SOURCES = $(wildcard src/*.java) +CLASSES = $(SOURCES:.java=.class) +MODEL_FILES = $(MODEL_DIR)/structural.mod +OUTPUT_FILE = $(INSTANCE_MODEL_DIR)/instances.mod + +## Makefile Rules ############################################################## +compile: $(CLASSES) + +model: $(CLASSES) $(INSTANCE_MODEL_DIR) $(OUTPUT_FILE) + +clean: + rm -f $(CLASSES) + rm -f $(PATH_MODEL_DIR)/*.mod + +clean_model: + rm -f $(PATH_MODEL_DIR)/*.mod +######## +%.class: %.java + $(JAVAC) -cp $(CLASSPATH) $< + +$(OUTPUT_FILE): $(MODEL_FILE) $(CLASSES) + $(JAVA) -cp $(CLASSPATH) Main $< $@ + +$(INSTANCE_MODEL_DIR): + mkdir -p $(INSTANCE_MODEL_DIR) + diff --git a/instance-calculator/src/.java_classpath b/instance-calculator/src/.java_classpath new file mode 100644 index 0000000..5e14ac9 --- /dev/null +++ b/instance-calculator/src/.java_classpath @@ -0,0 +1 @@ +../kodkod.jar diff --git a/instance-calculator/src/VHDLArchitecture.java b/instance-calculator/src/VHDLArchitecture.java new file mode 100644 index 0000000..ffd678c --- /dev/null +++ b/instance-calculator/src/VHDLArchitecture.java @@ -0,0 +1,22 @@ +import java.util.*; + +public class VHDLArchitecture +{ + private static final Map FROM_ID; + + static + { + FROM_ID = new HashMap(); + } + + private final List processes; + private final List components; + private final String id; + + private VHDLArchitecture (final String id) + { + this.id = id; + + ports = new ArrayList(); + } +} diff --git a/instance-calculator/src/VHDLComponent.java b/instance-calculator/src/VHDLComponent.java new file mode 100644 index 0000000..29261a7 --- /dev/null +++ b/instance-calculator/src/VHDLComponent.java @@ -0,0 +1,21 @@ +import java.util.*; + +public class VHDLComponent +{ + private static final Map FROM_ID; + + static + { + FROM_ID = new HashMap(); + } + + private final Map port_map; + private final String id; + + private VHDLComponent (final String id) + { + this.id = id; + + port_map = new HashMap(); + } +} diff --git a/instance-calculator/src/VHDLEntity.java b/instance-calculator/src/VHDLEntity.java new file mode 100644 index 0000000..c8fa332 --- /dev/null +++ b/instance-calculator/src/VHDLEntity.java @@ -0,0 +1,21 @@ +import java.util.*; + +public class VHDLEntity +{ + private static final Map FROM_ID; + + static + { + FROM_ID = new HashMap(); + } + + private final List ports; + private final String id; + + private VHDLEntity (final String id) + { + this.id = id; + + ports = new ArrayList(); + } +} diff --git a/instance-calculator/src/VHDLProcess.java b/instance-calculator/src/VHDLProcess.java new file mode 100644 index 0000000..f2f27e7 --- /dev/null +++ b/instance-calculator/src/VHDLProcess.java @@ -0,0 +1,21 @@ +import java.util.*; + +public class VHDLProcess +{ + private static final Map FROM_ID; + + static + { + FROM_ID = new HashMap(); + } + + private final List accessed_wfm; + private final String id; + + private VHDLProcess (final String id) + { + this.id = id; + + ports = new ArrayList(); + } +} -- cgit v1.2.3-70-g09d2 From f1dfb1eb04a705521238dba64e09bb9ecdea794f Mon Sep 17 00:00:00 2001 From: Nathanael Sensfelder Date: Tue, 29 Aug 2017 00:05:39 +0200 Subject: Starting to get an idea of how it's going to work. --- instance-calculator/src/Main.java | 85 +++++++++ instance-calculator/src/ModelFile.java | 262 ++++++++++++++++++++++++++ instance-calculator/src/Parameters.java | 63 +++++++ instance-calculator/src/ProcessInstance.java | 9 + instance-calculator/src/QuickParser.java | 58 ++++++ instance-calculator/src/VHDLArchitecture.java | 30 ++- instance-calculator/src/VHDLComponent.java | 28 +++ instance-calculator/src/VHDLEntity.java | 18 ++ instance-calculator/src/VHDLProcess.java | 19 ++ instance-calculator/src/Waveforms.java | 64 +++++++ 10 files changed, 635 insertions(+), 1 deletion(-) create mode 100644 instance-calculator/src/Main.java create mode 100644 instance-calculator/src/ModelFile.java create mode 100644 instance-calculator/src/Parameters.java create mode 100644 instance-calculator/src/ProcessInstance.java create mode 100644 instance-calculator/src/QuickParser.java create mode 100644 instance-calculator/src/Waveforms.java diff --git a/instance-calculator/src/Main.java b/instance-calculator/src/Main.java new file mode 100644 index 0000000..488b9bb --- /dev/null +++ b/instance-calculator/src/Main.java @@ -0,0 +1,85 @@ +/* FIXME: Finer imports */ +import java.util.*; + +import java.io.*; + +public class Main +{ + private static Parameters PARAMETERS; + + public static void main (final String... args) + { + final FileWriter output; + + PARAMETERS = new Parameters(args); + + if (!PARAMETERS.are_valid()) + { + return; + } + + try + { + ModelFile.load_file(PARAMETERS.get_model_file()); + } + catch (final Exception e) + { + System.err.println + ( + "[E] Could not load model file \"" + + PARAMETERS.get_model_file() + + "\":" + ); + + e.printStackTrace(); + + return; + } + } + + private static void create_instances () + { + /* + * FuturCandidates <- All Architecture. + * Candidates <- emptyset + * Set ProcessedCandidates <- emptyset. + * + * while (!isEmpty(FuturCandidates)) + * { + * is_stuck = True; + * Candidates.addAll(FuturCandidates); + * FuturCandidates.setLength(0); + * + * while (!isEmpty(candidates)) + * { + * a = Candidates.pop(); + * + * for (c: a.component) + * { + * if (!contains(c.target, ProcessedCandidates)) + * { + * FuturCandidates.push(a); + * continue; + * } + * } + * + * is_stuck = False; + * + * a.instantiate_all_processes(); + * + * for (c: a.component) + * { + * a.integrate_instanciated_processes_from(c); + * } + * + * ProcessedCandidates.add(a); + * } + * + * if (is_stuck) + * { + * Error. + * } + * } + */ + } +} diff --git a/instance-calculator/src/ModelFile.java b/instance-calculator/src/ModelFile.java new file mode 100644 index 0000000..7ca0899 --- /dev/null +++ b/instance-calculator/src/ModelFile.java @@ -0,0 +1,262 @@ +import java.io.*; + +public class ModelFile +{ + public static boolean load_file + ( + final String filename + ) + throws FileNotFoundException + { + final QuickParser qp; + String[] input; + boolean success; + + qp = new QuickParser(filename); + + for (;;) + { + try + { + input = qp.parse_line(); + + if (input == null) + { + qp.finalize(); + + return false; + } + else if (input.length == 0) + { + qp.finalize(); + + break; + } + } + catch (final IOException e) + { + System.err.println + ( + "[E] IO error while parsing file \"" + + filename + + "\":" + /* FIXME: can be null */ + + e.getMessage() + ); + + return false; + } + + if (input[0].equals("add_element")) + { + success = handle_add_element(input); + } + else if (input[0].equals("is_accessed_by")) + { + success = handle_is_accessed_by(input); + } + else if (input[0].equals("is_waveform_of")) + { + success = handle_is_waveform_of(input); + } + else if (input[0].equals("is_port_of")) + { + success = handle_is_port_of(input); + } + else if (input[0].equals("is_architecture_of")) + { + success = handle_is_architecture_of(input); + } + else if (input[0].equals("belongs_to_architecture")) + { + success = handle_belongs_to_architecture(input); + } + else if (input[0].equals("is_component_of")) + { + success = handle_is_component_of(input); + } + else if (input[0].equals("port_maps")) + { + success = handle_port_maps(input); + } + else + { + continue; + } + + if (!success) + { + System.err.println + ( + "[E] An erroneous instruction was found in file \"" + + filename + + "\"." + ); + + try + { + qp.finalize(); + } + catch (final Exception e) + { + System.err.println("[E] Additionally:"); + e.printStackTrace(); + } + + return false; + } + } + + return true; + } + + private static boolean handle_add_element + ( + final String[] input + ) + { + if (input.length != 3) + { + return false; + } + + if (input.equals("entity")) + { + VHDLEntity.add_element(input[2]); + } + else if (input.equals("architecture")) + { + VHDLArchitecture.add_element(input[2]); + } + else if (input.equals("process")) + { + VHDLProcess.add_element(input[2]); + } + else if (input.equals("component")) + { + VHDLComponent.add_element(input[2]); + } + + return true; + } + + private static boolean handle_is_accessed_by + ( + final String[] input + ) + { + if (input.length != 3) + { + return false; + } + + return VHDLProcess.handle_is_accessed_by(input[1], input[2]); + } + + private static boolean handle_is_waveform_of + ( + final String[] input + ) + { + if (input.length != 3) + { + return false; + } + + Waveforms.register_map(input[1], input[2]); + + return true; + } + + private static boolean handle_is_port_of + ( + final String[] input + ) + { + if (input.length != 3) + { + return false; + } + + VHDLEntity.handle_is_port_of(input[1], input[2]); + + return true; + } + + private static boolean handle_is_architecture_of + ( + final String[] input + ) + { + if (input.length != 3) + { + return false; + } + + VHDLArchitecture.handle_is_architecture_of(input[1], input[2]); + + return true; + } + + private static boolean handle_belongs_to_architecture + ( + final String[] input + ) + { + if (input.length != 3) + { + return false; + } + + VHDLArchitecture.handle_belongs_to_architecture(input[1], input[2]); + + return true; + } + + private static boolean handle_belongs_to_architecture + ( + final String[] input + ) + { + if (input.length != 3) + { + return false; + } + + VHDLArchitecture.handle_belongs_to_architecture(input[1], input[2]); + + return true; + } + + private static boolean handle_is_component_of + ( + final String[] input + ) + { + if (input.length != 3) + { + return false; + } + + VHDLComponent.handle_is_component_of(input[1], input[2]); + + return true; + } + + private static boolean handle_port_maps + ( + final String[] input + ) + { + if (input.length != 4) + { + return false; + } + + VHDLComponent.handle_port_maps(input[1], input[2], input[3]); + + return true; + } + + private ModelFile () {} /* Utility Class */ +} diff --git a/instance-calculator/src/Parameters.java b/instance-calculator/src/Parameters.java new file mode 100644 index 0000000..ce5e2cf --- /dev/null +++ b/instance-calculator/src/Parameters.java @@ -0,0 +1,63 @@ +public class Parameters +{ + private final String model_file; + private final String id_prefix; + private final String output_file; + private final boolean are_valid; + + public static void print_usage () + { + System.out.println + ( + "Instance-Calculator\n" + + "USAGE:\n" + + "\tjava Main \n" + + "PARAMETERS:\n" + + "\t\tInstruction file describing the model.\n" + + "\t\tPrefix for the IDs of generated paths.\n" + + "\t\tFile in which to output the generated" + + " instructions." + ); + } + + public Parameters (final String... args) + { + if (args.length != 4) + { + print_usage(); + + model_file = new String(); + id_prefix = new String(); + output_file = new String(); + + are_valid = false; + } + else + { + model_file = args[0]; + id_prefix = args[2]; + output_file = args[3]; + are_valid = true; + } + } + + public String get_model_file () + { + return model_file; + } + + public String get_id_prefix () + { + return id_prefix; + } + + public String get_output_file () + { + return output_file; + } + + public boolean are_valid () + { + return are_valid; + } +} diff --git a/instance-calculator/src/ProcessInstance.java b/instance-calculator/src/ProcessInstance.java new file mode 100644 index 0000000..580df6b --- /dev/null +++ b/instance-calculator/src/ProcessInstance.java @@ -0,0 +1,9 @@ +import java.util.*; + +public class ProcessInstance +{ + private final String id; + private String process_id; + private Map wfm_map; + +} diff --git a/instance-calculator/src/QuickParser.java b/instance-calculator/src/QuickParser.java new file mode 100644 index 0000000..47cea27 --- /dev/null +++ b/instance-calculator/src/QuickParser.java @@ -0,0 +1,58 @@ +/* FIXME: Finer imports */ +import java.io.*; +import java.util.regex.*; +import java.util.*; + +public class QuickParser +{ + private static final Pattern instr_pattern; + private final BufferedReader buffered_reader; + + static + { + instr_pattern = Pattern.compile("\\((?[a-z_0-9 \"]+)\\)"); + } + public QuickParser (final String filename) + throws FileNotFoundException + { + buffered_reader = new BufferedReader(new FileReader(filename)); + } + + public void finalize () + throws IOException + { + buffered_reader.close(); + } + + public String[] parse_line () + throws IOException + { + final List result; + final Matcher matcher; + String line; + + do + { + line = buffered_reader.readLine(); + + if (line == null) + { + return new String[0]; + } + + line = line.replaceAll("\\s+"," "); + } + while (line.length() < 3 || line.startsWith(";")); + + matcher = instr_pattern.matcher(line); + + if (!matcher.find()) + { + System.err.println("[E] Invalid instruction \"" + line + "\""); + + return null; + } + + return matcher.group(1).split(" |\t"); + } +} diff --git a/instance-calculator/src/VHDLArchitecture.java b/instance-calculator/src/VHDLArchitecture.java index ffd678c..2834ab3 100644 --- a/instance-calculator/src/VHDLArchitecture.java +++ b/instance-calculator/src/VHDLArchitecture.java @@ -9,6 +9,33 @@ public class VHDLArchitecture FROM_ID = new HashMap(); } + public static void add_element (final String id) + { + if (!FROM_ID.containsKey(id)) + { + FROM_ID.put(id, new VHDLArchitecture(id)); + } + } + + public static boolean handle_belongs_to_architecture + ( + final String unknown_id, + final String arch_id + ) + { + return false; + } + + public static boolean handle_is_architecture_of + ( + final String arch_id, + final String e_id + ) + { + return false; + } + +/******************************************************************************/ private final List processes; private final List components; private final String id; @@ -17,6 +44,7 @@ public class VHDLArchitecture { this.id = id; - ports = new ArrayList(); + processes = new ArrayList(); + components = new ArrayList(); } } diff --git a/instance-calculator/src/VHDLComponent.java b/instance-calculator/src/VHDLComponent.java index 29261a7..493ba22 100644 --- a/instance-calculator/src/VHDLComponent.java +++ b/instance-calculator/src/VHDLComponent.java @@ -9,6 +9,34 @@ public class VHDLComponent FROM_ID = new HashMap(); } + public static void add_element (final String id) + { + if (!FROM_ID.containsKey(id)) + { + FROM_ID.put(id, new VHDLComponent(id)); + } + } + + public static boolean handle_is_component_of + ( + final String cmp_id, + final String e_id + ) + { + return false; + } + + public static boolean handle_port_maps + ( + final String cmp_id, + final String pt_id, + final String wfm_id + ) + { + return false; + } + +/******************************************************************************/ private final Map port_map; private final String id; diff --git a/instance-calculator/src/VHDLEntity.java b/instance-calculator/src/VHDLEntity.java index c8fa332..a5ba28c 100644 --- a/instance-calculator/src/VHDLEntity.java +++ b/instance-calculator/src/VHDLEntity.java @@ -9,6 +9,24 @@ public class VHDLEntity FROM_ID = new HashMap(); } + public static void add_element (final String id) + { + if (!FROM_ID.containsKey(id)) + { + FROM_ID.put(id, new VHDLEntity(id)); + } + } + + public static boolean handle_is_port_of + ( + final String pt_id, + final String e_id + ) + { + return false; + } + +/******************************************************************************/ private final List ports; private final String id; diff --git a/instance-calculator/src/VHDLProcess.java b/instance-calculator/src/VHDLProcess.java index f2f27e7..a017ef4 100644 --- a/instance-calculator/src/VHDLProcess.java +++ b/instance-calculator/src/VHDLProcess.java @@ -9,6 +9,25 @@ public class VHDLProcess FROM_ID = new HashMap(); } + public static void add_element (final String id) + { + if (!FROM_ID.containsKey(id)) + { + FROM_ID.put(id, new VHDLProcess(id)); + } + } + + public static boolean handle_is_accessed_by + ( + final String wfm_id, + final String ps_id + ) + { + return false; + } + +/******************************************************************************/ + private final List accessed_wfm; private final String id; diff --git a/instance-calculator/src/Waveforms.java b/instance-calculator/src/Waveforms.java new file mode 100644 index 0000000..e7a4c8c --- /dev/null +++ b/instance-calculator/src/Waveforms.java @@ -0,0 +1,64 @@ +import java.util.Map; +import java.util.HashMap; + +public class Waveforms +{ + private static final Map FROM_WAVEFORM; + private static final Map TO_WAVEFORM; + + static + { + FROM_WAVEFORM = new HashMap(); + TO_WAVEFORM = new HashMap(); + } + + private Waveforms () {} /* Utility class. */ + + public static void register_map (final String wfm_id, final String elem_id) + { + FROM_WAVEFORM.put(wfm_id, elem_id); + TO_WAVEFORM.put(elem_id, wfm_id); + } + + public static String get_id_from_waveform_id (final String wfm_id) + { + final String result; + + result = FROM_WAVEFORM.get(wfm_id); + + if (result == null) + { + System.err.println + ( + "[F] There is no element associated with waveform \"" + + wfm_id + + "\". Is the model complete?" + ); + + System.exit(-1); + } + + return result; + } + + public static String get_waveform_id_from_id (final String src_id) + { + final String result; + + result = TO_WAVEFORM.get(src_id); + + if (result == null) + { + System.err.println + ( + "[F] There is no waveform associated with the element \"" + + src_id + + "\". Is the model complete?" + ); + + System.exit(-1); + } + + return result; + } +} -- cgit v1.2.3-70-g09d2 From 35e6857fb09b006da9f8cc3f59f239f078cc69a1 Mon Sep 17 00:00:00 2001 From: Nathanael Sensfelder Date: Tue, 29 Aug 2017 13:54:43 +0200 Subject: Still working on the implementation. --- instance-calculator/src/Instances.java | 30 ++++++++ instance-calculator/src/Main.java | 26 ++++--- instance-calculator/src/ModelFile.java | 36 ++-------- instance-calculator/src/ProcessInstance.java | 9 --- instance-calculator/src/VHDLArchitecture.java | 9 +++ instance-calculator/src/VHDLComponent.java | 60 ++++++++++++++++ instance-calculator/src/VHDLEntity.java | 30 +++++++- instance-calculator/src/VHDLProcess.java | 76 +++++++++++++++++++- instance-calculator/src/VHDLWaveform.java | 99 +++++++++++++++++++++++++++ 9 files changed, 318 insertions(+), 57 deletions(-) create mode 100644 instance-calculator/src/Instances.java delete mode 100644 instance-calculator/src/ProcessInstance.java create mode 100644 instance-calculator/src/VHDLWaveform.java diff --git a/instance-calculator/src/Instances.java b/instance-calculator/src/Instances.java new file mode 100644 index 0000000..5d6ec8b --- /dev/null +++ b/instance-calculator/src/Instances.java @@ -0,0 +1,30 @@ +import java.util.*; + +public class Instances +{ + private static final Map instances; + + static + { + instances = new HashMap(); + } + + public static String get_id_for (final int i) + { + final Integer j; + String result; + + j = new Integer(i); + + result = instances.get(j); + + if (result == null) + { + result = (Main.get_parameters().get_id_prefix() + i); + + instances.put(j, result); + } + + return result; + } +} diff --git a/instance-calculator/src/Main.java b/instance-calculator/src/Main.java index 488b9bb..3835c16 100644 --- a/instance-calculator/src/Main.java +++ b/instance-calculator/src/Main.java @@ -54,25 +54,18 @@ public class Main * { * a = Candidates.pop(); * - * for (c: a.component) + * if (a.has_components_not_in(ProcessedCandidates)) * { - * if (!contains(c.target, ProcessedCandidates)) - * { - * FuturCandidates.push(a); - * continue; - * } + * FuturCandidates.push(a); * } + * else + * { + * is_stuck = False; * - * is_stuck = False; - * - * a.instantiate_all_processes(); + * a.create_instance(); * - * for (c: a.component) - * { - * a.integrate_instanciated_processes_from(c); + * ProcessedCandidates.add(a); * } - * - * ProcessedCandidates.add(a); * } * * if (is_stuck) @@ -82,4 +75,9 @@ public class Main * } */ } + + public static Parameters get_parameters () + { + return PARAMETERS; + } } diff --git a/instance-calculator/src/ModelFile.java b/instance-calculator/src/ModelFile.java index 7ca0899..691de1a 100644 --- a/instance-calculator/src/ModelFile.java +++ b/instance-calculator/src/ModelFile.java @@ -178,9 +178,7 @@ public class ModelFile return false; } - VHDLEntity.handle_is_port_of(input[1], input[2]); - - return true; + return VHDLEntity.handle_is_port_of(input[1], input[2]); } private static boolean handle_is_architecture_of @@ -193,24 +191,7 @@ public class ModelFile return false; } - VHDLArchitecture.handle_is_architecture_of(input[1], input[2]); - - return true; - } - - private static boolean handle_belongs_to_architecture - ( - final String[] input - ) - { - if (input.length != 3) - { - return false; - } - - VHDLArchitecture.handle_belongs_to_architecture(input[1], input[2]); - - return true; + return VHDLArchitecture.handle_is_architecture_of(input[1], input[2]); } private static boolean handle_belongs_to_architecture @@ -223,9 +204,8 @@ public class ModelFile return false; } - VHDLArchitecture.handle_belongs_to_architecture(input[1], input[2]); - - return true; + return + VHDLArchitecture.handle_belongs_to_architecture(input[1], input[2]); } private static boolean handle_is_component_of @@ -238,9 +218,7 @@ public class ModelFile return false; } - VHDLComponent.handle_is_component_of(input[1], input[2]); - - return true; + return VHDLComponent.handle_is_component_of(input[1], input[2]); } private static boolean handle_port_maps @@ -253,9 +231,7 @@ public class ModelFile return false; } - VHDLComponent.handle_port_maps(input[1], input[2], input[3]); - - return true; + return VHDLComponent.handle_port_maps(input[1], input[2], input[3]); } private ModelFile () {} /* Utility Class */ diff --git a/instance-calculator/src/ProcessInstance.java b/instance-calculator/src/ProcessInstance.java deleted file mode 100644 index 580df6b..0000000 --- a/instance-calculator/src/ProcessInstance.java +++ /dev/null @@ -1,9 +0,0 @@ -import java.util.*; - -public class ProcessInstance -{ - private final String id; - private String process_id; - private Map wfm_map; - -} diff --git a/instance-calculator/src/VHDLArchitecture.java b/instance-calculator/src/VHDLArchitecture.java index 2834ab3..7f3be10 100644 --- a/instance-calculator/src/VHDLArchitecture.java +++ b/instance-calculator/src/VHDLArchitecture.java @@ -23,6 +23,7 @@ public class VHDLArchitecture final String arch_id ) { + /* TODO */ return false; } @@ -32,6 +33,7 @@ public class VHDLArchitecture final String e_id ) { + /* TODO */ return false; } @@ -40,6 +42,8 @@ public class VHDLArchitecture private final List components; private final String id; + private VHDLEntity entity; + private VHDLArchitecture (final String id) { this.id = id; @@ -47,4 +51,9 @@ public class VHDLArchitecture processes = new ArrayList(); components = new ArrayList(); } + + public VHDLEntity get_entity () + { + return entity; + } } diff --git a/instance-calculator/src/VHDLComponent.java b/instance-calculator/src/VHDLComponent.java index 493ba22..5972173 100644 --- a/instance-calculator/src/VHDLComponent.java +++ b/instance-calculator/src/VHDLComponent.java @@ -23,6 +23,7 @@ public class VHDLComponent final String e_id ) { + /* TODO */ return false; } @@ -33,6 +34,7 @@ public class VHDLComponent final String wfm_id ) { + /* TODO */ return false; } @@ -40,6 +42,64 @@ public class VHDLComponent private final Map port_map; private final String id; + private VHDLEntity destination; + private VHDLArchitecture parent; + + public void add_instance_content_to + ( + final Collection process_instances, + final Collection waveform_instances + ) + { + final Collection dest_process_instances; + final Collection dest_waveform_instances; + final Map wfm_map; + + dest_process_instances = destination.get_process_instances(); + dest_waveform_instances = destination.get_waveform_instances(); + + wfm_map = new HashMap(); + + for (final VHDLWaveform.Instance i_wfm: dest_waveform_instances) + { + final String dest; + final VHDLWaveform.Instance replacement; + + dest = + port_map.get + ( + Waveforms.get_id_from_waveform_id + ( + i_wfm.get_parent().get_id() + ) + ); + + if (dest == null) + { + replacement = i_wfm.get_parent().add_instance(parent.get_entity()); + } + else + { + replacement = + VHDLWaveform.get_from_id(dest).add_instance + ( + parent.get_entity() + ); + } + + wfm_map.put(i_wfm, replacement); + waveform_instances.add(replacement); + } + + for (final VHDLProcess.Instance i_ps: dest_process_instances) + { + process_instances.add + ( + i_ps.add_instance(parent.get_entity(), wfm_map) + ); + } + } + private VHDLComponent (final String id) { this.id = id; diff --git a/instance-calculator/src/VHDLEntity.java b/instance-calculator/src/VHDLEntity.java index a5ba28c..8059566 100644 --- a/instance-calculator/src/VHDLEntity.java +++ b/instance-calculator/src/VHDLEntity.java @@ -23,17 +23,45 @@ public class VHDLEntity final String e_id ) { + /* TODO */ + return false; + } + + public static boolean handle_is_architecture_of + ( + final String pt_id, + final String e_id + ) + { + /* TODO */ return false; } /******************************************************************************/ + private final Collection process_instances; + private final Collection waveform_instances; + private final List ports; private final String id; + private String architecture; + private VHDLEntity (final String id) { this.id = id; - ports = new ArrayList(); + + this.process_instances = new ArrayList(); + this.waveform_instances = new ArrayList(); + } + + public Collection get_process_instances () + { + return process_instances; + } + + public Collection get_waveform_instances () + { + return waveform_instances; } } diff --git a/instance-calculator/src/VHDLProcess.java b/instance-calculator/src/VHDLProcess.java index a017ef4..f85fe9a 100644 --- a/instance-calculator/src/VHDLProcess.java +++ b/instance-calculator/src/VHDLProcess.java @@ -23,18 +23,88 @@ public class VHDLProcess final String ps_id ) { + /* TODO */ return false; } /******************************************************************************/ - - private final List accessed_wfm; + private final Collection accessed_wfm; + private final Collection instances; private final String id; + private int instances_count; private VHDLProcess (final String id) { this.id = id; + accessed_wfm = new ArrayList(); + instances = new ArrayList(); + instances_count = 0; + } + + public static class Instance + { + private final String id; + private final VHDLProcess parent; + private final Map iwfm_map; + private final VHDLEntity visibility; + + private Instance + ( + final String id, + final VHDLProcess parent, + final VHDLEntity visibility, + final Map iwfm_map + ) + { + this.id = id; + this.parent = parent; + this.visibility = visibility; + this.iwfm_map = iwfm_map; + } + + public VHDLProcess get_parent () + { + return parent; + } + + public VHDLProcess.Instance add_instance + ( + final VHDLEntity visibility, + final Map convertion + ) + { + final VHDLProcess.Instance result; + final Set> iwfm_set; + final Map new_iwfm_map; + + iwfm_set = iwfm_map.entrySet(); + + new_iwfm_map = new HashMap(); - ports = new ArrayList(); + for + ( + final Map.Entry me: iwfm_set + ) + { + new_iwfm_map.put + ( + convertion.get(me.getKey()), + me.getValue() + ); + } + + result = + new VHDLProcess.Instance + ( + Instances.get_id_for(parent.instances_count), + parent, + visibility, + new_iwfm_map + ); + + parent.instances_count += 1; + + return result; + } } } diff --git a/instance-calculator/src/VHDLWaveform.java b/instance-calculator/src/VHDLWaveform.java new file mode 100644 index 0000000..83b9626 --- /dev/null +++ b/instance-calculator/src/VHDLWaveform.java @@ -0,0 +1,99 @@ +import java.util.*; + +public class VHDLWaveform +{ + private static final Map FROM_ID; + + static + { + FROM_ID = new HashMap(); + } + + public static void add_element (final String id) + { + if (!FROM_ID.containsKey(id)) + { + FROM_ID.put(id, new VHDLWaveform(id)); + } + } + + public static VHDLWaveform get_from_id (final String id) + { + return FROM_ID.get(id); + } + + public static boolean handle_is_accessed_by + ( + final String wfm_id, + final String ps_id + ) + { + /* TODO */ + return false; + } + +/******************************************************************************/ + private final Collection accessed_wfm; + private final Collection instances; + private final String id; + private int instances_count; + + private VHDLWaveform (final String id) + { + this.id = id; + accessed_wfm = new ArrayList(); + instances = new ArrayList(); + instances_count = 0; + } + + public VHDLWaveform.Instance add_instance + ( + final VHDLEntity visibility + ) + { + final VHDLWaveform.Instance result; + + result = + new VHDLWaveform.Instance + ( + Instances.get_id_for(instances_count), + this, + visibility + ); + + instances.add(result); + + instances_count += 1; + + return result; + } + + public String get_id () + { + return id; + } + + public static class Instance + { + private final String id; + private final VHDLWaveform parent; + private final VHDLEntity visibility; + + private Instance + ( + final String id, + final VHDLWaveform parent, + final VHDLEntity visibility + ) + { + this.id = id; + this.parent = parent; + this.visibility = visibility; + } + + public VHDLWaveform get_parent () + { + return parent; + } + } +} -- cgit v1.2.3-70-g09d2 From 9a5e79dfd1c6829b052ab7cf0cb7a79afd25eb72 Mon Sep 17 00:00:00 2001 From: Nathanael Sensfelder Date: Tue, 29 Aug 2017 15:23:34 +0200 Subject: Should now load the model. --- instance-calculator/src/ModelFile.java | 91 ++++++++++++++++++++++++--- instance-calculator/src/VHDLArchitecture.java | 74 ++++++++++++++++------ instance-calculator/src/VHDLComponent.java | 51 ++++++++++----- instance-calculator/src/VHDLEntity.java | 54 +++++++++++----- instance-calculator/src/VHDLProcess.java | 47 +++++++++++--- instance-calculator/src/VHDLWaveform.java | 36 ++++++++--- instance-calculator/src/Waveforms.java | 10 +++ 7 files changed, 292 insertions(+), 71 deletions(-) diff --git a/instance-calculator/src/ModelFile.java b/instance-calculator/src/ModelFile.java index 691de1a..929c348 100644 --- a/instance-calculator/src/ModelFile.java +++ b/instance-calculator/src/ModelFile.java @@ -145,12 +145,28 @@ public class ModelFile final String[] input ) { + final VHDLProcess ps; + final VHDLWaveform wfm; + if (input.length != 3) { return false; } - return VHDLProcess.handle_is_accessed_by(input[1], input[2]); + ps = VHDLProcess.get_from_id(input[2]); + wfm = VHDLWaveform.find(input[1]); + + if (wfm != null) + { + /* + * Assumes that otherwise it's a string, but that could also be due to + * an inconsistent model. + */ + + ps.add_accessed_wfm(wfm); + } + + return true; } private static boolean handle_is_waveform_of @@ -178,7 +194,9 @@ public class ModelFile return false; } - return VHDLEntity.handle_is_port_of(input[1], input[2]); + VHDLEntity.get_from_id(input[2]).add_port(input[1]); + + return true; } private static boolean handle_is_architecture_of @@ -186,12 +204,21 @@ public class ModelFile final String[] input ) { + final VHDLEntity e; + final VHDLArchitecture arch; + if (input.length != 3) { return false; } - return VHDLArchitecture.handle_is_architecture_of(input[1], input[2]); + e = VHDLEntity.get_from_id(input[2]); + arch = VHDLArchitecture.get_from_id(input[1]); + + e.set_architecture(arch); + arch.set_entity(e); + + return true; } private static boolean handle_belongs_to_architecture @@ -199,13 +226,52 @@ public class ModelFile final String[] input ) { + final VHDLArchitecture arch; + final VHDLProcess ps; + final VHDLComponent cmp; + final String wfm_id; + final VHDLWaveform wfm; + if (input.length != 3) { return false; } - return - VHDLArchitecture.handle_belongs_to_architecture(input[1], input[2]); + arch = VHDLArchitecture.get_from_id(input[2]); + + ps = VHDLProcess.find(input[1]); + + if (ps != null) + { + arch.add_process(ps); + ps.set_architecture(arch); + + return true; + } + + cmp = VHDLComponent.find(input[1]); + + if (cmp != null) + { + arch.add_component(cmp); + cmp.set_architecture(arch); + + return true; + } + + wfm_id = Waveforms.find_waveform_id_from_id(input[1]); + + if (wfm_id != null) + { + wfm = VHDLWaveform.get_from_id(wfm_id); + + arch.add_waveform(wfm); + wfm.set_architecture(arch); + + return true; + } + + return true; } private static boolean handle_is_component_of @@ -218,7 +284,12 @@ public class ModelFile return false; } - return VHDLComponent.handle_is_component_of(input[1], input[2]); + VHDLComponent.get_from_id(input[1]).set_destination + ( + VHDLEntity.get_from_id(input[2]) + ); + + return true; } private static boolean handle_port_maps @@ -231,7 +302,13 @@ public class ModelFile return false; } - return VHDLComponent.handle_port_maps(input[1], input[2], input[3]); + VHDLComponent.get_from_id(input[1]).add_port_map + ( + input[2], + input[3] + ); + + return true; } private ModelFile () {} /* Utility Class */ diff --git a/instance-calculator/src/VHDLArchitecture.java b/instance-calculator/src/VHDLArchitecture.java index 7f3be10..0a61a24 100644 --- a/instance-calculator/src/VHDLArchitecture.java +++ b/instance-calculator/src/VHDLArchitecture.java @@ -17,29 +17,37 @@ public class VHDLArchitecture } } - public static boolean handle_belongs_to_architecture - ( - final String unknown_id, - final String arch_id - ) + public static VHDLArchitecture get_from_id (final String id) { - /* TODO */ - return false; + final VHDLArchitecture result; + + result = FROM_ID.get(id); + + if (result == null) + { + System.err.println + ( + "[E] Element " + + id + + " is used like an architecture, but is not declared as such" + + " before that use." + ); + + System.exit(-1); + } + + return result; } - public static boolean handle_is_architecture_of - ( - final String arch_id, - final String e_id - ) + public static VHDLArchitecture find (final String id) { - /* TODO */ - return false; + return FROM_ID.get(id); } /******************************************************************************/ - private final List processes; - private final List components; + private final Collection processes; + private final Collection components; + private final Collection waveforms; private final String id; private VHDLEntity entity; @@ -48,12 +56,42 @@ public class VHDLArchitecture { this.id = id; - processes = new ArrayList(); - components = new ArrayList(); + processes = new ArrayList(); + components = new ArrayList(); + waveforms = new ArrayList(); } public VHDLEntity get_entity () { return entity; } + + public void set_entity (final VHDLEntity e) + { + entity = e; + } + + public void add_process (final VHDLProcess ps) + { + if (!processes.contains(ps)) + { + processes.add(ps); + } + } + + public void add_component (final VHDLComponent cmp) + { + if (!components.contains(cmp)) + { + components.add(cmp); + } + } + + public void add_waveform (final VHDLWaveform wfm) + { + if (!waveforms.contains(wfm)) + { + waveforms.add(wfm); + } + } } diff --git a/instance-calculator/src/VHDLComponent.java b/instance-calculator/src/VHDLComponent.java index 5972173..b0f8de2 100644 --- a/instance-calculator/src/VHDLComponent.java +++ b/instance-calculator/src/VHDLComponent.java @@ -17,25 +17,31 @@ public class VHDLComponent } } - public static boolean handle_is_component_of - ( - final String cmp_id, - final String e_id - ) + public static VHDLComponent get_from_id (final String id) { - /* TODO */ - return false; + final VHDLComponent result; + + result = FROM_ID.get(id); + + if (result == null) + { + System.err.println + ( + "[E] Element " + + id + + " is used like a component instantiation, but is not declared as" + + " such before that use." + ); + + System.exit(-1); + } + + return result; } - public static boolean handle_port_maps - ( - final String cmp_id, - final String pt_id, - final String wfm_id - ) + public static VHDLComponent find (final String id) { - /* TODO */ - return false; + return FROM_ID.get(id); } /******************************************************************************/ @@ -45,6 +51,21 @@ public class VHDLComponent private VHDLEntity destination; private VHDLArchitecture parent; + public void set_destination (final VHDLEntity dest) + { + destination = dest; + } + + public void set_architecture (final VHDLArchitecture arch) + { + parent = arch; + } + + public void add_port_map (final String src, final String dest) + { + port_map.put(src, dest); + } + public void add_instance_content_to ( final Collection process_instances, diff --git a/instance-calculator/src/VHDLEntity.java b/instance-calculator/src/VHDLEntity.java index 8059566..e5ab4eb 100644 --- a/instance-calculator/src/VHDLEntity.java +++ b/instance-calculator/src/VHDLEntity.java @@ -17,44 +17,66 @@ public class VHDLEntity } } - public static boolean handle_is_port_of - ( - final String pt_id, - final String e_id - ) + public static VHDLEntity get_from_id (final String id) { - /* TODO */ - return false; + final VHDLEntity result; + + result = FROM_ID.get(id); + + if (result == null) + { + System.err.println + ( + "[E] Element " + + id + + " is used like an entity, but is not declared as such before that" + + " use." + ); + + System.exit(-1); + } + + return result; } - public static boolean handle_is_architecture_of - ( - final String pt_id, - final String e_id - ) + public static VHDLEntity find (final String id) { - /* TODO */ - return false; + return FROM_ID.get(id); } /******************************************************************************/ private final Collection process_instances; private final Collection waveform_instances; - private final List ports; + private final Collection ports; private final String id; - private String architecture; + private VHDLArchitecture architecture; private VHDLEntity (final String id) { this.id = id; ports = new ArrayList(); + architecture = null; + this.process_instances = new ArrayList(); this.waveform_instances = new ArrayList(); } + public void add_port (final String pt) + { + if (!ports.contains(pt)) + { + ports.add(pt); + } + } + + public void set_architecture (final VHDLArchitecture arch) + { + architecture = arch; + } + public Collection get_process_instances () { return process_instances; diff --git a/instance-calculator/src/VHDLProcess.java b/instance-calculator/src/VHDLProcess.java index f85fe9a..5466dbb 100644 --- a/instance-calculator/src/VHDLProcess.java +++ b/instance-calculator/src/VHDLProcess.java @@ -17,14 +17,31 @@ public class VHDLProcess } } - public static boolean handle_is_accessed_by - ( - final String wfm_id, - final String ps_id - ) + public static VHDLProcess get_from_id (final String id) { - /* TODO */ - return false; + final VHDLProcess result; + + result = FROM_ID.get(id); + + if (result == null) + { + System.err.println + ( + "[E] Element " + + id + + " is used like a process, but is not declared as such before that" + + " use." + ); + + System.exit(-1); + } + + return result; + } + + public static VHDLProcess find (final String id) + { + return FROM_ID.get(id); } /******************************************************************************/ @@ -33,12 +50,28 @@ public class VHDLProcess private final String id; private int instances_count; + private VHDLArchitecture architecture; + private VHDLProcess (final String id) { this.id = id; accessed_wfm = new ArrayList(); instances = new ArrayList(); instances_count = 0; + architecture = null; + } + + public void add_accessed_wfm (final VHDLWaveform wfm) + { + if (!accessed_wfm.contains(wfm)) + { + accessed_wfm.add(wfm); + } + } + + public void set_architecture (final VHDLArchitecture arch) + { + architecture = arch; } public static class Instance diff --git a/instance-calculator/src/VHDLWaveform.java b/instance-calculator/src/VHDLWaveform.java index 83b9626..1f29b99 100644 --- a/instance-calculator/src/VHDLWaveform.java +++ b/instance-calculator/src/VHDLWaveform.java @@ -19,17 +19,29 @@ public class VHDLWaveform public static VHDLWaveform get_from_id (final String id) { - return FROM_ID.get(id); + final VHDLWaveform result; + + result = FROM_ID.get(id); + + if (result == null) + { + System.err.println + ( + "[E] Element " + + id + + " is used like a waveform, but is not declared as such before" + + " that use." + ); + + System.exit(-1); + } + + return result; } - public static boolean handle_is_accessed_by - ( - final String wfm_id, - final String ps_id - ) + public static VHDLWaveform find (final String id) { - /* TODO */ - return false; + return FROM_ID.get(id); } /******************************************************************************/ @@ -38,12 +50,15 @@ public class VHDLWaveform private final String id; private int instances_count; + private VHDLArchitecture architecture; + private VHDLWaveform (final String id) { this.id = id; accessed_wfm = new ArrayList(); instances = new ArrayList(); instances_count = 0; + architecture = null; } public VHDLWaveform.Instance add_instance @@ -73,6 +88,11 @@ public class VHDLWaveform return id; } + public void set_architecture (final VHDLArchitecture arch) + { + architecture = arch; + } + public static class Instance { private final String id; diff --git a/instance-calculator/src/Waveforms.java b/instance-calculator/src/Waveforms.java index e7a4c8c..9492d16 100644 --- a/instance-calculator/src/Waveforms.java +++ b/instance-calculator/src/Waveforms.java @@ -61,4 +61,14 @@ public class Waveforms return result; } + + public static String find_id_from_waveform_id (final String wfm_id) + { + return FROM_WAVEFORM.get(wfm_id); + } + + public static String find_waveform_id_from_id (final String src_id) + { + return TO_WAVEFORM.get(src_id); + } } -- cgit v1.2.3-70-g09d2 From ea11fdc81ed7a8df14868476c04bf2fe7c7b6393 Mon Sep 17 00:00:00 2001 From: Nathanael Sensfelder Date: Tue, 29 Aug 2017 16:51:09 +0200 Subject: Most of the program's logic seems to be there... --- Makefile | 7 ++ instance-calculator/Makefile | 11 ++- instance-calculator/src/Main.java | 104 +++++++++++++++++--------- instance-calculator/src/ModelFile.java | 8 +- instance-calculator/src/Parameters.java | 6 +- instance-calculator/src/VHDLArchitecture.java | 5 ++ instance-calculator/src/VHDLComponent.java | 5 ++ instance-calculator/src/VHDLEntity.java | 19 +++++ 8 files changed, 120 insertions(+), 45 deletions(-) diff --git a/Makefile b/Makefile index 19a69d8..ecaee82 100644 --- a/Makefile +++ b/Makefile @@ -12,6 +12,7 @@ SOL_DIR = $(TMP_DIR)/sol ## Sub-programs ################################################################ AST_TO_INSTR = ast-to-instr +INST_CALC = instance-calculator SOLVER = instr-to-kodkod PRETTY_PRINTER = sol-pretty-printer @@ -24,31 +25,37 @@ all: $(TMP_DIR) $(MODEL_DIR) $(SOL_DIR) compile: $(MAKE) -C $(AST_TO_INSTR) compile + $(MAKE) -C $(INST_CALC) compile $(MAKE) -C $(SOLVER) compile $(MAKE) -C $(PRETTY_PRINTER) compile model: $(MAKE) -C $(AST_TO_INSTR) model + $(MAKE) -C $(INST_CALC) model $(MAKE) -C $(SOLVER) model $(MAKE) -C $(PRETTY_PRINTER) model solutions: $(TMP_DIR) $(MODEL_DIR) $(SOL_DIR) $(MAKE) -C $(AST_TO_INSTR) solutions + $(MAKE) -C $(INST_CALC) solutions $(MAKE) -C $(SOLVER) solutions $(MAKE) -C $(PRETTY_PRINTER) solutions clean: $(MAKE) -C $(AST_TO_INSTR) clean + $(MAKE) -C $(INST_CALC) clean $(MAKE) -C $(SOLVER) clean $(MAKE) -C $(PRETTY_PRINTER) clean clean_model: $(MAKE) -C $(AST_TO_INSTR) clean_model + $(MAKE) -C $(INST_CALC) clean_model $(MAKE) -C $(SOLVER) clean_model $(MAKE) -C $(PRETTY_PRINTER) clean_model clean_solutions: $(MAKE) -C $(AST_TO_INSTR) clean_solutions + $(MAKE) -C $(INST_CALC) clean_solutions $(MAKE) -C $(SOLVER) clean_solutions $(MAKE) -C $(PRETTY_PRINTER) clean_solutions diff --git a/instance-calculator/Makefile b/instance-calculator/Makefile index 8da7891..356b681 100644 --- a/instance-calculator/Makefile +++ b/instance-calculator/Makefile @@ -6,7 +6,7 @@ endif #### Where to store the Instance model ifndef INSTANCE_MODEL_DIR -INSTANCE_MODEL_DIR = +INSTANCE_MODEL_DIR = $(MODEL_DIR)/instance/ endif #### Binaries @@ -43,7 +43,7 @@ CLASSPATH = "./src/" ## Makefile Magic ############################################################## SOURCES = $(wildcard src/*.java) CLASSES = $(SOURCES:.java=.class) -MODEL_FILES = $(MODEL_DIR)/structural.mod +MODEL_FILE = $(MODEL_DIR)/structural.mod OUTPUT_FILE = $(INSTANCE_MODEL_DIR)/instances.mod ## Makefile Rules ############################################################## @@ -51,18 +51,23 @@ compile: $(CLASSES) model: $(CLASSES) $(INSTANCE_MODEL_DIR) $(OUTPUT_FILE) +solutions: + clean: rm -f $(CLASSES) rm -f $(PATH_MODEL_DIR)/*.mod clean_model: rm -f $(PATH_MODEL_DIR)/*.mod + +clean_solutions: + ######## %.class: %.java $(JAVAC) -cp $(CLASSPATH) $< $(OUTPUT_FILE): $(MODEL_FILE) $(CLASSES) - $(JAVA) -cp $(CLASSPATH) Main $< $@ + $(JAVA) -cp $(CLASSPATH) Main $(MODEL_FILE) "inst_" $@ $(INSTANCE_MODEL_DIR): mkdir -p $(INSTANCE_MODEL_DIR) diff --git a/instance-calculator/src/Main.java b/instance-calculator/src/Main.java index 3835c16..b521324 100644 --- a/instance-calculator/src/Main.java +++ b/instance-calculator/src/Main.java @@ -35,45 +35,79 @@ public class Main return; } + + create_instances(); } private static void create_instances () { - /* - * FuturCandidates <- All Architecture. - * Candidates <- emptyset - * Set ProcessedCandidates <- emptyset. - * - * while (!isEmpty(FuturCandidates)) - * { - * is_stuck = True; - * Candidates.addAll(FuturCandidates); - * FuturCandidates.setLength(0); - * - * while (!isEmpty(candidates)) - * { - * a = Candidates.pop(); - * - * if (a.has_components_not_in(ProcessedCandidates)) - * { - * FuturCandidates.push(a); - * } - * else - * { - * is_stuck = False; - * - * a.create_instance(); - * - * ProcessedCandidates.add(a); - * } - * } - * - * if (is_stuck) - * { - * Error. - * } - * } - */ + final Collection futur_candidates; + final Deque candidates; + final Collection processed_candidates; + boolean is_stuck; + + futur_candidates = new ArrayList(); + candidates = new ArrayDeque(); + processed_candidates = new ArrayList(); + + futur_candidates.addAll(VHDLEntity.get_all()); + + while (!futur_candidates.isEmpty()) + { + is_stuck = true; + + candidates.addAll(futur_candidates); + futur_candidates.clear(); + + while (!candidates.isEmpty()) + { + final VHDLEntity e; + boolean is_ready; + + e = candidates.pop(); + + is_ready = true; + + for (final VHDLComponent cmp: e.get_architecture().get_components()) + { + if (!processed_candidates.contains(cmp.get_destination())) + { + is_ready = false; + + break; + } + } + + if (is_ready) + { + is_stuck = false; + + e.generate_instance(); + + processed_candidates.add(e); + } + else + { + futur_candidates.add(e); + } + } + + if (is_stuck) + { + System.err.println("[F] Unable to create all the instances..."); + System.err.println + ( + "[E] The following entites might form a circular dependency:" + ); + + for (final VHDLEntity e: futur_candidates) + { + System.err.println("[E] Entity " + e.get_id()); + } + + System.exit(-1); + } + } } public static Parameters get_parameters () diff --git a/instance-calculator/src/ModelFile.java b/instance-calculator/src/ModelFile.java index 929c348..b873c3b 100644 --- a/instance-calculator/src/ModelFile.java +++ b/instance-calculator/src/ModelFile.java @@ -120,19 +120,19 @@ public class ModelFile return false; } - if (input.equals("entity")) + if (input[1].equals("entity")) { VHDLEntity.add_element(input[2]); } - else if (input.equals("architecture")) + else if (input[1].equals("architecture")) { VHDLArchitecture.add_element(input[2]); } - else if (input.equals("process")) + else if (input[1].equals("process")) { VHDLProcess.add_element(input[2]); } - else if (input.equals("component")) + else if (input[1].equals("component")) { VHDLComponent.add_element(input[2]); } diff --git a/instance-calculator/src/Parameters.java b/instance-calculator/src/Parameters.java index ce5e2cf..e01f912 100644 --- a/instance-calculator/src/Parameters.java +++ b/instance-calculator/src/Parameters.java @@ -22,7 +22,7 @@ public class Parameters public Parameters (final String... args) { - if (args.length != 4) + if (args.length != 3) { print_usage(); @@ -35,8 +35,8 @@ public class Parameters else { model_file = args[0]; - id_prefix = args[2]; - output_file = args[3]; + id_prefix = args[1]; + output_file = args[2]; are_valid = true; } } diff --git a/instance-calculator/src/VHDLArchitecture.java b/instance-calculator/src/VHDLArchitecture.java index 0a61a24..09576e3 100644 --- a/instance-calculator/src/VHDLArchitecture.java +++ b/instance-calculator/src/VHDLArchitecture.java @@ -87,6 +87,11 @@ public class VHDLArchitecture } } + public Collection get_components () + { + return components; + } + public void add_waveform (final VHDLWaveform wfm) { if (!waveforms.contains(wfm)) diff --git a/instance-calculator/src/VHDLComponent.java b/instance-calculator/src/VHDLComponent.java index b0f8de2..6803a57 100644 --- a/instance-calculator/src/VHDLComponent.java +++ b/instance-calculator/src/VHDLComponent.java @@ -56,6 +56,11 @@ public class VHDLComponent destination = dest; } + public VHDLEntity get_destination () + { + return destination; + } + public void set_architecture (final VHDLArchitecture arch) { parent = arch; diff --git a/instance-calculator/src/VHDLEntity.java b/instance-calculator/src/VHDLEntity.java index e5ab4eb..7c29e63 100644 --- a/instance-calculator/src/VHDLEntity.java +++ b/instance-calculator/src/VHDLEntity.java @@ -9,6 +9,11 @@ public class VHDLEntity FROM_ID = new HashMap(); } + public static Collection get_all () + { + return FROM_ID.values(); + } + public static void add_element (final String id) { if (!FROM_ID.containsKey(id)) @@ -64,6 +69,11 @@ public class VHDLEntity this.waveform_instances = new ArrayList(); } + public String get_id () + { + return id; + } + public void add_port (final String pt) { if (!ports.contains(pt)) @@ -77,6 +87,11 @@ public class VHDLEntity architecture = arch; } + public VHDLArchitecture get_architecture () + { + return architecture; + } + public Collection get_process_instances () { return process_instances; @@ -86,4 +101,8 @@ public class VHDLEntity { return waveform_instances; } + + public void generate_instance () + { + } } -- cgit v1.2.3-70-g09d2 From 882d605d684abf7120a1b5b095e7f5425e77dd34 Mon Sep 17 00:00:00 2001 From: Nathanael Sensfelder Date: Tue, 29 Aug 2017 17:59:53 +0200 Subject: Seems like all remains is doing the actual output. --- instance-calculator/src/ModelFile.java | 4 +++ instance-calculator/src/VHDLArchitecture.java | 41 +++++++++++++++++++++++++++ instance-calculator/src/VHDLComponent.java | 7 +++-- instance-calculator/src/VHDLEntity.java | 23 +++++++++++++++ instance-calculator/src/VHDLProcess.java | 33 +++++++++++++++++++++ instance-calculator/src/VHDLWaveform.java | 2 ++ 6 files changed, 107 insertions(+), 3 deletions(-) diff --git a/instance-calculator/src/ModelFile.java b/instance-calculator/src/ModelFile.java index b873c3b..8589116 100644 --- a/instance-calculator/src/ModelFile.java +++ b/instance-calculator/src/ModelFile.java @@ -128,6 +128,10 @@ public class ModelFile { VHDLArchitecture.add_element(input[2]); } + else if (input[1].equals("waveform")) + { + VHDLWaveform.add_element(input[2]); + } else if (input[1].equals("process")) { VHDLProcess.add_element(input[2]); diff --git a/instance-calculator/src/VHDLArchitecture.java b/instance-calculator/src/VHDLArchitecture.java index 09576e3..5597529 100644 --- a/instance-calculator/src/VHDLArchitecture.java +++ b/instance-calculator/src/VHDLArchitecture.java @@ -99,4 +99,45 @@ public class VHDLArchitecture waveforms.add(wfm); } } + + public void add_instance_to + ( + final Collection process_instances, + final Collection waveform_instances, + final Map local_conversion + ) + { + for (final VHDLWaveform wfm: waveforms) + { + final VHDLWaveform.Instance i_wfm; + + i_wfm = wfm.add_instance(entity); + + waveform_instances.add(i_wfm); + + local_conversion.put(wfm, i_wfm); + } + + for (final VHDLProcess ps: processes) + { + process_instances.add + ( + ps.generate_base_instance + ( + entity, + waveform_instances + ) + ); + } + + for (final VHDLComponent cmp: components) + { + cmp.add_instance_content_to + ( + process_instances, + waveform_instances, + local_conversion + ); + } + } } diff --git a/instance-calculator/src/VHDLComponent.java b/instance-calculator/src/VHDLComponent.java index 6803a57..fb05c6e 100644 --- a/instance-calculator/src/VHDLComponent.java +++ b/instance-calculator/src/VHDLComponent.java @@ -74,7 +74,8 @@ public class VHDLComponent public void add_instance_content_to ( final Collection process_instances, - final Collection waveform_instances + final Collection waveform_instances, + final Map local_conversion ) { final Collection dest_process_instances; @@ -107,9 +108,9 @@ public class VHDLComponent else { replacement = - VHDLWaveform.get_from_id(dest).add_instance + local_conversion.get ( - parent.get_entity() + Waveforms.get_waveform_id_from_id(dest) ); } diff --git a/instance-calculator/src/VHDLEntity.java b/instance-calculator/src/VHDLEntity.java index 7c29e63..91de6f6 100644 --- a/instance-calculator/src/VHDLEntity.java +++ b/instance-calculator/src/VHDLEntity.java @@ -104,5 +104,28 @@ public class VHDLEntity public void generate_instance () { + final Map local_conversion; + + local_conversion = new HashMap(); + + for (final String pt: ports) + { + final VHDLWaveform wfm; + final VHDLWaveform.Instance i_wfm; + + wfm = VHDLWaveform.get_from_id(Waveforms.get_waveform_id_from_id(pt)); + i_wfm = wfm.add_instance(this); + + waveform_instances.add(i_wfm); + + local_conversion.put(wfm, i_wfm); + } + + architecture.add_instance_to + ( + process_instances, + waveform_instances, + local_conversion + ); } } diff --git a/instance-calculator/src/VHDLProcess.java b/instance-calculator/src/VHDLProcess.java index 5466dbb..d54e0cc 100644 --- a/instance-calculator/src/VHDLProcess.java +++ b/instance-calculator/src/VHDLProcess.java @@ -74,6 +74,39 @@ public class VHDLProcess architecture = arch; } + public VHDLProcess.Instance generate_base_instance + ( + final VHDLEntity visibility, + final Collection waveform_instances + ) + { + final VHDLProcess.Instance result; + final Map iwfm_map; + + iwfm_map = new HashMap(); + + for (final VHDLWaveform.Instance i_wfm: waveform_instances) + { + if (accessed_wfm.contains(i_wfm.get_parent())) + { + iwfm_map.put(i_wfm, i_wfm.get_parent()); + } + } + + result = + new VHDLProcess.Instance + ( + Instances.get_id_for(instances_count), + this, + visibility, + iwfm_map + ); + + instances_count += 1; + + return result; + } + public static class Instance { private final String id; diff --git a/instance-calculator/src/VHDLWaveform.java b/instance-calculator/src/VHDLWaveform.java index 1f29b99..eb5c38e 100644 --- a/instance-calculator/src/VHDLWaveform.java +++ b/instance-calculator/src/VHDLWaveform.java @@ -33,6 +33,8 @@ public class VHDLWaveform + " that use." ); + new Exception().printStackTrace(); + System.exit(-1); } -- cgit v1.2.3-70-g09d2 From aebd8f1bd52495b0a787e0cccfa4501141eace2b Mon Sep 17 00:00:00 2001 From: Nathanael Sensfelder Date: Wed, 30 Aug 2017 11:22:16 +0200 Subject: Outputs are now generated. --- instance-calculator/Makefile | 2 +- instance-calculator/src/Instances.java | 22 ++++- instance-calculator/src/Main.java | 3 + instance-calculator/src/ModelFile.java | 16 +-- instance-calculator/src/OutputFile.java | 135 ++++++++++++++++++++++++++ instance-calculator/src/Parameters.java | 17 ++-- instance-calculator/src/VHDLArchitecture.java | 31 ++++++ instance-calculator/src/VHDLComponent.java | 31 +++--- instance-calculator/src/VHDLEntity.java | 17 ++++ instance-calculator/src/VHDLProcess.java | 63 ++++++++++++ instance-calculator/src/VHDLWaveform.java | 51 ++++++++++ 11 files changed, 350 insertions(+), 38 deletions(-) create mode 100644 instance-calculator/src/OutputFile.java diff --git a/instance-calculator/Makefile b/instance-calculator/Makefile index 356b681..25d31cc 100644 --- a/instance-calculator/Makefile +++ b/instance-calculator/Makefile @@ -67,7 +67,7 @@ clean_solutions: $(JAVAC) -cp $(CLASSPATH) $< $(OUTPUT_FILE): $(MODEL_FILE) $(CLASSES) - $(JAVA) -cp $(CLASSPATH) Main $(MODEL_FILE) "inst_" $@ + $(JAVA) -cp $(CLASSPATH) Main $(MODEL_FILE) "inst_" $(INSTANCE_MODEL_DIR) $(INSTANCE_MODEL_DIR): mkdir -p $(INSTANCE_MODEL_DIR) diff --git a/instance-calculator/src/Instances.java b/instance-calculator/src/Instances.java index 5d6ec8b..d4954d9 100644 --- a/instance-calculator/src/Instances.java +++ b/instance-calculator/src/Instances.java @@ -2,11 +2,13 @@ import java.util.*; public class Instances { - private static final Map instances; + private static final Map INSTANCES; + private static final OutputFile OUTPUT_FILE; static { - instances = new HashMap(); + INSTANCES = new HashMap(); + OUTPUT_FILE = OutputFile.new_output_file("instances.mod"); } public static String get_id_for (final int i) @@ -16,15 +18,27 @@ public class Instances j = new Integer(i); - result = instances.get(j); + result = INSTANCES.get(j); if (result == null) { result = (Main.get_parameters().get_id_prefix() + i); - instances.put(j, result); + INSTANCES.put(j, result); } return result; } + + public static void write_predicates () + { + for (final String id: INSTANCES.values()) + { + OUTPUT_FILE.write("(add_element instance "); + OUTPUT_FILE.write(id); + OUTPUT_FILE.write(")"); + + OUTPUT_FILE.insert_newline(); + } + } } diff --git a/instance-calculator/src/Main.java b/instance-calculator/src/Main.java index b521324..a23da06 100644 --- a/instance-calculator/src/Main.java +++ b/instance-calculator/src/Main.java @@ -37,6 +37,8 @@ public class Main } create_instances(); + Instances.write_predicates(); + OutputFile.close_all(); } private static void create_instances () @@ -84,6 +86,7 @@ public class Main e.generate_instance(); + e.write_predicates(); processed_candidates.add(e); } else diff --git a/instance-calculator/src/ModelFile.java b/instance-calculator/src/ModelFile.java index 8589116..1f9297e 100644 --- a/instance-calculator/src/ModelFile.java +++ b/instance-calculator/src/ModelFile.java @@ -107,6 +107,8 @@ public class ModelFile } } + VHDLArchitecture.resolve_all_waveforms(); + return true; } @@ -233,8 +235,6 @@ public class ModelFile final VHDLArchitecture arch; final VHDLProcess ps; final VHDLComponent cmp; - final String wfm_id; - final VHDLWaveform wfm; if (input.length != 3) { @@ -263,17 +263,7 @@ public class ModelFile return true; } - wfm_id = Waveforms.find_waveform_id_from_id(input[1]); - - if (wfm_id != null) - { - wfm = VHDLWaveform.get_from_id(wfm_id); - - arch.add_waveform(wfm); - wfm.set_architecture(arch); - - return true; - } + arch.add_futur_waveform(input[1]); return true; } diff --git a/instance-calculator/src/OutputFile.java b/instance-calculator/src/OutputFile.java new file mode 100644 index 0000000..201ca2b --- /dev/null +++ b/instance-calculator/src/OutputFile.java @@ -0,0 +1,135 @@ +import java.util.ArrayList; +import java.util.Collection; + +import java.io.File; +import java.io.FileWriter; +import java.io.BufferedWriter; + +public class OutputFile +{ + private static Collection ALL_OUTPUT_FILES; + + static + { + ALL_OUTPUT_FILES = new ArrayList(); + } + + public static void close_all () + { + for (final OutputFile f: ALL_OUTPUT_FILES) + { + f.close(); + } + } + + public static OutputFile new_output_file (final String filename) + { + final OutputFile result; + + result = + new OutputFile + ( + Main.get_parameters().get_output_directory() + + "/" + + filename + ); + + ALL_OUTPUT_FILES.add(result); + + return result; + } + + /** Non-Static *************************************************************/ + private final String filename; + private final BufferedWriter buffered_writer; + + private OutputFile (final String filename) + { + BufferedWriter bf; + + this.filename = filename; + + try + { + bf = new BufferedWriter(new FileWriter(new File(filename))); + } + catch (final Exception e) + { + bf = null; + + System.err.println + ( + "[F] Could not create new output file \"" + + filename + + "\":" + ); + + e.printStackTrace(); + + System.exit(-1); + } + + buffered_writer = bf; + } + + public void write (final String data) + { + try + { + buffered_writer.write(data); + } + catch (final Exception e) + { + System.err.println + ( + "[F] Could not write to output file \"" + + filename + + "\":" + ); + + e.printStackTrace(); + + System.exit(-1); + } + } + + public void insert_newline () + { + try + { + buffered_writer.newLine(); + } + catch (final Exception e) + { + System.err.println + ( + "[F] Could not write to output file \"" + + filename + + "\":" + ); + + e.printStackTrace(); + + System.exit(-1); + } + } + + private void close () + { + try + { + buffered_writer.close(); + } + catch (final Exception e) + { + System.err.println + ( + "[E] Could not properly close output file \"" + + filename + + "\":" + ); + + e.printStackTrace(); + } + } +} diff --git a/instance-calculator/src/Parameters.java b/instance-calculator/src/Parameters.java index e01f912..b8bba30 100644 --- a/instance-calculator/src/Parameters.java +++ b/instance-calculator/src/Parameters.java @@ -2,7 +2,7 @@ public class Parameters { private final String model_file; private final String id_prefix; - private final String output_file; + private final String output_dir; private final boolean are_valid; public static void print_usage () @@ -11,12 +11,12 @@ public class Parameters ( "Instance-Calculator\n" + "USAGE:\n" - + "\tjava Main \n" + + "\tjava Main \n" + "PARAMETERS:\n" + "\t\tInstruction file describing the model.\n" + "\t\tPrefix for the IDs of generated paths.\n" - + "\t\tFile in which to output the generated" - + " instructions." + + "\t\tDirectory in which to output the generated" + + " instruction files." ); } @@ -28,7 +28,7 @@ public class Parameters model_file = new String(); id_prefix = new String(); - output_file = new String(); + output_dir = new String(); are_valid = false; } @@ -36,7 +36,8 @@ public class Parameters { model_file = args[0]; id_prefix = args[1]; - output_file = args[2]; + output_dir = args[2]; + are_valid = true; } } @@ -51,9 +52,9 @@ public class Parameters return id_prefix; } - public String get_output_file () + public String get_output_directory () { - return output_file; + return output_dir; } public boolean are_valid () diff --git a/instance-calculator/src/VHDLArchitecture.java b/instance-calculator/src/VHDLArchitecture.java index 5597529..407a09f 100644 --- a/instance-calculator/src/VHDLArchitecture.java +++ b/instance-calculator/src/VHDLArchitecture.java @@ -9,6 +9,14 @@ public class VHDLArchitecture FROM_ID = new HashMap(); } + public static void resolve_all_waveforms () + { + for (final VHDLArchitecture arch: FROM_ID.values()) + { + arch.resolve_waveforms(); + } + } + public static void add_element (final String id) { if (!FROM_ID.containsKey(id)) @@ -48,6 +56,7 @@ public class VHDLArchitecture private final Collection processes; private final Collection components; private final Collection waveforms; + private final Deque futur_waveforms; private final String id; private VHDLEntity entity; @@ -59,6 +68,7 @@ public class VHDLArchitecture processes = new ArrayList(); components = new ArrayList(); waveforms = new ArrayList(); + futur_waveforms = new ArrayDeque(); } public VHDLEntity get_entity () @@ -100,6 +110,27 @@ public class VHDLArchitecture } } + public void add_futur_waveform (final String fwfm) + { + if (!futur_waveforms.contains(fwfm)) + { + futur_waveforms.add(fwfm); + } + } + + public void resolve_waveforms () + { + while (!futur_waveforms.isEmpty()) + { + final String src_id, wfm_id; + + src_id = futur_waveforms.pop(); + + wfm_id = Waveforms.get_waveform_id_from_id(src_id); + add_waveform(VHDLWaveform.get_from_id(wfm_id)); + } + } + public void add_instance_to ( final Collection process_instances, diff --git a/instance-calculator/src/VHDLComponent.java b/instance-calculator/src/VHDLComponent.java index fb05c6e..958a2e4 100644 --- a/instance-calculator/src/VHDLComponent.java +++ b/instance-calculator/src/VHDLComponent.java @@ -45,7 +45,7 @@ public class VHDLComponent } /******************************************************************************/ - private final Map port_map; + private final Map reverse_port_map; private final String id; private VHDLEntity destination; @@ -68,7 +68,7 @@ public class VHDLComponent public void add_port_map (final String src, final String dest) { - port_map.put(src, dest); + reverse_port_map.put(dest, src); } public void add_instance_content_to @@ -89,28 +89,35 @@ public class VHDLComponent for (final VHDLWaveform.Instance i_wfm: dest_waveform_instances) { - final String dest; + final String src_wfm, dest_port; final VHDLWaveform.Instance replacement; - dest = - port_map.get + dest_port = + Waveforms.get_id_from_waveform_id ( - Waveforms.get_id_from_waveform_id - ( - i_wfm.get_parent().get_id() - ) + i_wfm.get_parent().get_id() ); - if (dest == null) + src_wfm = reverse_port_map.get(dest_port); + + if (src_wfm == null) { + /* i_wfm is not linked to a port, so it needs a new instance. */ replacement = i_wfm.get_parent().add_instance(parent.get_entity()); } else { + /* + * i_wfm is linked to a port. Replace it by what's connected to the + * port. + */ replacement = local_conversion.get ( - Waveforms.get_waveform_id_from_id(dest) + VHDLWaveform.get_from_id + ( + src_wfm + ) ); } @@ -131,6 +138,6 @@ public class VHDLComponent { this.id = id; - port_map = new HashMap(); + reverse_port_map = new HashMap(); } } diff --git a/instance-calculator/src/VHDLEntity.java b/instance-calculator/src/VHDLEntity.java index 91de6f6..2765229 100644 --- a/instance-calculator/src/VHDLEntity.java +++ b/instance-calculator/src/VHDLEntity.java @@ -1,4 +1,5 @@ import java.util.*; +import java.io.BufferedWriter; public class VHDLEntity { @@ -53,6 +54,7 @@ public class VHDLEntity private final Collection process_instances; private final Collection waveform_instances; + private final OutputFile output_file; private final Collection ports; private final String id; @@ -67,6 +69,8 @@ public class VHDLEntity this.process_instances = new ArrayList(); this.waveform_instances = new ArrayList(); + + output_file = OutputFile.new_output_file("instances_in_" + id + ".mod"); } public String get_id () @@ -128,4 +132,17 @@ public class VHDLEntity local_conversion ); } + + public void write_predicates () + { + for (final VHDLWaveform.Instance iwfm: waveform_instances) + { + iwfm.write_predicates_to(output_file); + } + + for (final VHDLProcess.Instance ips: process_instances) + { + ips.write_predicates_to(output_file); + } + } } diff --git a/instance-calculator/src/VHDLProcess.java b/instance-calculator/src/VHDLProcess.java index d54e0cc..eba5e46 100644 --- a/instance-calculator/src/VHDLProcess.java +++ b/instance-calculator/src/VHDLProcess.java @@ -1,4 +1,5 @@ import java.util.*; +import java.io.BufferedWriter; public class VHDLProcess { @@ -61,6 +62,11 @@ public class VHDLProcess architecture = null; } + public String get_id () + { + return id; + } + public void add_accessed_wfm (final VHDLWaveform wfm) { if (!accessed_wfm.contains(wfm)) @@ -172,5 +178,62 @@ public class VHDLProcess return result; } + + public void write_predicates_to (final OutputFile of) + { + final Set> iwfm_set; + + iwfm_set = iwfm_map.entrySet(); + + try + { + of.write("(is_process_instance "); + of.write(id); + of.write(" "); + of.write(parent.get_id()); + of.write(")"); + of.insert_newline(); + + of.write("(is_visible_in "); + of.write(id); + of.write(" "); + of.write(parent.get_id()); + of.write(" "); + of.write(visibility.get_id()); + of.write(")"); + of.insert_newline(); + + for + ( + final Map.Entry iwfm: + iwfm_set + ) + { + of.write("(process_instance_maps "); + of.write(id); + of.write(" "); + of.write(parent.get_id()); + of.write(" "); + of.write(iwfm.getKey().get_id()); + of.write(" "); + of.write(iwfm.getKey().get_parent().get_id()); + of.write(" "); + of.write(iwfm.getValue().get_id()); + of.write(")"); + of.insert_newline(); + } + } + catch (final Exception e) + { + System.err.println + ( + "[F] Could not write to output file:" + ); + + e.printStackTrace(); + + System.exit(-1); + } + } } } diff --git a/instance-calculator/src/VHDLWaveform.java b/instance-calculator/src/VHDLWaveform.java index eb5c38e..74edc88 100644 --- a/instance-calculator/src/VHDLWaveform.java +++ b/instance-calculator/src/VHDLWaveform.java @@ -1,4 +1,5 @@ import java.util.*; +import java.io.BufferedWriter; public class VHDLWaveform { @@ -95,6 +96,12 @@ public class VHDLWaveform architecture = arch; } + @Override + public String toString () + { + return id; + } + public static class Instance { private final String id; @@ -113,9 +120,53 @@ public class VHDLWaveform this.visibility = visibility; } + public String get_id () + { + return id; + } + public VHDLWaveform get_parent () { return parent; } + + public void write_predicates_to (final OutputFile of) + { + try + { + of.write("(is_waveform_instance "); + of.write(id); + of.write(" "); + of.write(parent.get_id()); + of.write(")"); + of.insert_newline(); + + of.write("(is_visible_in "); + of.write(id); + of.write(" "); + of.write(parent.get_id()); + of.write(" "); + of.write(visibility.get_id()); + of.write(")"); + of.insert_newline(); + } + catch (final Exception e) + { + System.err.println + ( + "[F] Could not write to output file:" + ); + + e.printStackTrace(); + + System.exit(-1); + } + } + + @Override + public String toString () + { + return "<" + parent.get_id() + ", " + id + ">"; + } } } -- cgit v1.2.3-70-g09d2 From b715c825c0a36063e7b79248059263b438a0b5a6 Mon Sep 17 00:00:00 2001 From: Nathanael Sensfelder Date: Wed, 30 Aug 2017 13:57:53 +0200 Subject: Gets stuck due to scaling issues. --- Makefile | 5 +++-- data/level/instances.lvl | 22 ++++++++++++++++++++++ instance-calculator/Makefile | 18 +++++++++--------- instr-to-kodkod/Makefile | 4 +++- 4 files changed, 37 insertions(+), 12 deletions(-) create mode 100644 data/level/instances.lvl diff --git a/Makefile b/Makefile index ecaee82..4a18566 100644 --- a/Makefile +++ b/Makefile @@ -1,13 +1,14 @@ ## Makefile Parameters ######################################################### LEVEL_FILES = $(wildcard ${CURDIR}/data/level/*.lvl) PROPERTY_FILES = \ - $(wildcard ${CURDIR}/data/property/*.pro) \ - $(wildcard ${CURDIR}/data/property/cnes/*.pro) + $(wildcard ${CURDIR}/data/property/*.pro) +# $(wildcard ${CURDIR}/data/property/cnes/*.pro) AST_FILE = ${CURDIR}/data/ast/best_chronometer_ever.xml #AST_FILE = ${CURDIR}/data/ast/pong.xml TMP_DIR = /tmp/tabellion MODEL_DIR = $(TMP_DIR)/mod +MODEL_INSTANCES_DIR = $(TMP_DIR)/instance SOL_DIR = $(TMP_DIR)/sol ## Sub-programs ################################################################ diff --git a/data/level/instances.lvl b/data/level/instances.lvl new file mode 100644 index 0000000..5fdb42b --- /dev/null +++ b/data/level/instances.lvl @@ -0,0 +1,22 @@ +;; Instances + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; TYPES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(add_type instance) + +;; Redundancies +(add_type entity) +(add_type process) +(add_type waveform) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; PREDICATES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(add_predicate is_waveform_instance instance waveform) +(add_predicate is_visible_in instance waveform entity) + +(add_predicate is_process_instance instance process) +(add_predicate is_visible_in instance process entity) + +(add_predicate process_instance_maps instance process instance waveform waveform) diff --git a/instance-calculator/Makefile b/instance-calculator/Makefile index 25d31cc..5f25d1a 100644 --- a/instance-calculator/Makefile +++ b/instance-calculator/Makefile @@ -5,8 +5,8 @@ MODEL_DIR = endif #### Where to store the Instance model -ifndef INSTANCE_MODEL_DIR -INSTANCE_MODEL_DIR = $(MODEL_DIR)/instance/ +ifndef MODEL_INSTANCES_DIR +MODEL_INSTANCES_DIR = endif #### Binaries @@ -25,8 +25,8 @@ ifeq ($(strip $(MODEL_DIR)),) $(error No MODEL_DIR defined as parameter.) endif -ifeq ($(strip $(INSTANCE_MODEL_DIR)),) -$(error No INSTANCE_MODEL_DIR defined as parameter.) +ifeq ($(strip $(MODEL_INSTANCES_DIR)),) +$(error No MODEL_INSTANCES_DIR defined as parameter.) endif ifeq ($(strip $(JAVA)),) @@ -44,12 +44,12 @@ CLASSPATH = "./src/" SOURCES = $(wildcard src/*.java) CLASSES = $(SOURCES:.java=.class) MODEL_FILE = $(MODEL_DIR)/structural.mod -OUTPUT_FILE = $(INSTANCE_MODEL_DIR)/instances.mod +OUTPUT_FILE = $(MODEL_INSTANCES_DIR)/instances.mod ## Makefile Rules ############################################################## compile: $(CLASSES) -model: $(CLASSES) $(INSTANCE_MODEL_DIR) $(OUTPUT_FILE) +model: $(CLASSES) $(MODEL_INSTANCES_DIR) $(OUTPUT_FILE) solutions: @@ -67,8 +67,8 @@ clean_solutions: $(JAVAC) -cp $(CLASSPATH) $< $(OUTPUT_FILE): $(MODEL_FILE) $(CLASSES) - $(JAVA) -cp $(CLASSPATH) Main $(MODEL_FILE) "inst_" $(INSTANCE_MODEL_DIR) + $(JAVA) -cp $(CLASSPATH) Main $(MODEL_FILE) "inst_" $(MODEL_INSTANCES_DIR) -$(INSTANCE_MODEL_DIR): - mkdir -p $(INSTANCE_MODEL_DIR) +$(MODEL_INSTANCES_DIR): + mkdir -p $(MODEL_INSTANCES_DIR) diff --git a/instr-to-kodkod/Makefile b/instr-to-kodkod/Makefile index 03e451a..8543ee4 100644 --- a/instr-to-kodkod/Makefile +++ b/instr-to-kodkod/Makefile @@ -95,7 +95,9 @@ MODEL_FILES = \ $(MODEL_DIR)/structural.mod \ $(MODEL_DIR)/depths.mod \ $(MODEL_DIR)/string_to_instr.map \ - $(filter-out %structural.mod,$(wildcard $(MODEL_DIR)/cfg_*.mod)) + $(wildcard $(MODEL_DIR)/cfg_*.mod) \ + $(MODEL_INSTANCES_DIR)/instances.mod \ + $(wildcard $(MODEL_INSTANCESDIR)/instances_in_*.mod) PARSER_SOURCES = $(wildcard parser/*.g4) PARSER_CLASSES = $(PARSER_SOURCES:.g4=.class) -- cgit v1.2.3-70-g09d2 From 99bbe050e57c50c5c21b849c1721fe9979894d8f Mon Sep 17 00:00:00 2001 From: Nathanael Sensfelder Date: Wed, 30 Aug 2017 15:15:02 +0200 Subject: Reduces the scalability issue. It seems to take very long to find solutions for simple_flip_flop_instance, but at least it no longer gives up right away. --- Makefile | 2 +- data/level/instances.lvl | 13 ++-- data/property/simple_flip_flop_instance.pp | 6 ++ data/property/simple_flip_flop_instance.pro | 95 +++++++++++++++++++++++++++++ instance-calculator/Makefile | 7 ++- instance-calculator/src/Instances.java | 44 ------------- instance-calculator/src/Main.java | 1 - instance-calculator/src/VHDLProcess.java | 31 ++++++---- instance-calculator/src/VHDLWaveform.java | 30 ++++++--- instr-to-kodkod/Makefile | 3 +- 10 files changed, 157 insertions(+), 75 deletions(-) create mode 100644 data/property/simple_flip_flop_instance.pp create mode 100644 data/property/simple_flip_flop_instance.pro delete mode 100644 instance-calculator/src/Instances.java diff --git a/Makefile b/Makefile index 4a18566..116e4ec 100644 --- a/Makefile +++ b/Makefile @@ -8,7 +8,7 @@ AST_FILE = ${CURDIR}/data/ast/best_chronometer_ever.xml TMP_DIR = /tmp/tabellion MODEL_DIR = $(TMP_DIR)/mod -MODEL_INSTANCES_DIR = $(TMP_DIR)/instance +MODEL_INSTANCES_DIR = $(MODEL_DIR)/instance SOL_DIR = $(TMP_DIR)/sol ## Sub-programs ################################################################ diff --git a/data/level/instances.lvl b/data/level/instances.lvl index 5fdb42b..ad6e93f 100644 --- a/data/level/instances.lvl +++ b/data/level/instances.lvl @@ -3,7 +3,8 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; TYPES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(add_type instance) +(add_type wfm_instance) +(add_type ps_instance) ;; Redundancies (add_type entity) @@ -13,10 +14,10 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; PREDICATES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(add_predicate is_waveform_instance instance waveform) -(add_predicate is_visible_in instance waveform entity) +(add_predicate is_wfm_instance_of wfm_instance waveform) +(add_predicate is_visible_in wfm_instance entity) -(add_predicate is_process_instance instance process) -(add_predicate is_visible_in instance process entity) +(add_predicate is_ps_instance_of ps_instance process) +(add_predicate is_visible_in ps_instance entity) -(add_predicate process_instance_maps instance process instance waveform waveform) +(add_predicate process_instance_maps ps_instance wfm_instance waveform) diff --git a/data/property/simple_flip_flop_instance.pp b/data/property/simple_flip_flop_instance.pp new file mode 100644 index 0000000..b460eec --- /dev/null +++ b/data/property/simple_flip_flop_instance.pp @@ -0,0 +1,6 @@ +The component described by the entity $ent.IDENTIFIER$ (declared in $ent.FILE$, +line $ent.LINE$, column $ent.COLUMN$) has a simple flip-flop described by the +process $ps.LABEL$ (declared in $ps.FILE$, l. $ps.LINE$, c. $ps.COLUMN$), +controlled by $clk.IDENTIFIER$ (declared in $clk.FILE$, l. $clk.LINE$, +c. $clk.COLUMN$), and with output $reg.IDENTIFIER$ (declared in $reg.FILE$, +l. $reg.LINE$, c. $reg.COLUMN$). diff --git a/data/property/simple_flip_flop_instance.pro b/data/property/simple_flip_flop_instance.pro new file mode 100644 index 0000000..a3881aa --- /dev/null +++ b/data/property/simple_flip_flop_instance.pro @@ -0,0 +1,95 @@ +(tag_existing + ( + (ent entity STRUCT_ENTITY) + (reg waveform STRUCT_SIMPLE_FLIP_FLOP_OUTPUT) + (clk waveform STRUCT_SIMPLE_FLIP_FLOP_CLOCK) + (ps process STRUCT_SIMPLE_FLIP_FLOP_PROCESS) + ) + (and + (is_explicit_process ps) +;; debt: )) +;; Get ps instance +(exists i_ps ps_instance + (and + (is_visible_in i_ps ent) + (is_ps_instance_of i_ps ps) +;; debt: )) )) +;; Get a local waveform matching a clk instance +(exists i_clk wfm_instance + (and + (process_instance_maps i_ps i_clk _) +;; (is_visible_in i_clk ent) + (is_wfm_instance_of i_clk clk) + (exists local_clk waveform + (and + (process_instance_maps i_ps i_clk local_clk) + (is_in_sensitivity_list local_clk ps) +;; debt: )))) )))) +;; Get a local waveform matching a reg instance +(exists i_reg wfm_instance + (and + (process_instance_maps i_ps i_reg _) +;; (is_visible_in i_reg ent) + (is_wfm_instance_of i_reg reg) + (exists local_reg waveform + (and + (process_instance_maps i_ps i_reg local_reg) +;; debt: )))) )))))))) +;; Analyze ps using the local waveforms +(CTL_verifies ps + (AF + (and + (kind "if") + (or + (and + (is_read_structure "(??)") + (or + (is_read_element "0" "falling_edge") + (is_read_element "0" "rising_edge") + ) + (is_read_element "1" local_clk) + ) + (and + (is_read_structure "(?(??)(???))") + (is_read_element "0" "and") + (is_read_element "1" "event") + (is_read_element "2" local_clk) + (is_read_element "3" "=") + (or + (is_read_element "4" local_clk) + (is_read_element "5" local_clk) + ) + ) + (and + (is_read_structure "(?(???)(??))") + (is_read_element "0" "and") + (is_read_element "1" "=") + (or + (is_read_element "2" local_clk) + (is_read_element "3" local_clk) + ) + (is_read_element "4" "event") + (is_read_element "5" local_clk) + ) + ) + (EX + (and + (has_option "COND_WAS_TRUE") + (does_not_reach_parent_before + (and + (expr_writes local_reg) + (AX + (not + (EF + (expr_writes local_reg) + ) + ) + ) + ) + ) + ) + ) + ) + ) +) +)))))))))))) diff --git a/instance-calculator/Makefile b/instance-calculator/Makefile index 5f25d1a..9dddc88 100644 --- a/instance-calculator/Makefile +++ b/instance-calculator/Makefile @@ -44,7 +44,7 @@ CLASSPATH = "./src/" SOURCES = $(wildcard src/*.java) CLASSES = $(SOURCES:.java=.class) MODEL_FILE = $(MODEL_DIR)/structural.mod -OUTPUT_FILE = $(MODEL_INSTANCES_DIR)/instances.mod +OUTPUT_FILE = $(MODEL_INSTANCES_DIR)/witness ## Makefile Rules ############################################################## compile: $(CLASSES) @@ -55,10 +55,10 @@ solutions: clean: rm -f $(CLASSES) - rm -f $(PATH_MODEL_DIR)/*.mod + rm -f $(MODEL_INSTANCES_DIR)/* clean_model: - rm -f $(PATH_MODEL_DIR)/*.mod + rm -f $(MODEL_INSTANCES_DIR)/* clean_solutions: @@ -68,6 +68,7 @@ clean_solutions: $(OUTPUT_FILE): $(MODEL_FILE) $(CLASSES) $(JAVA) -cp $(CLASSPATH) Main $(MODEL_FILE) "inst_" $(MODEL_INSTANCES_DIR) + touch $(OUTPUT_FILE) $(MODEL_INSTANCES_DIR): mkdir -p $(MODEL_INSTANCES_DIR) diff --git a/instance-calculator/src/Instances.java b/instance-calculator/src/Instances.java deleted file mode 100644 index d4954d9..0000000 --- a/instance-calculator/src/Instances.java +++ /dev/null @@ -1,44 +0,0 @@ -import java.util.*; - -public class Instances -{ - private static final Map INSTANCES; - private static final OutputFile OUTPUT_FILE; - - static - { - INSTANCES = new HashMap(); - OUTPUT_FILE = OutputFile.new_output_file("instances.mod"); - } - - public static String get_id_for (final int i) - { - final Integer j; - String result; - - j = new Integer(i); - - result = INSTANCES.get(j); - - if (result == null) - { - result = (Main.get_parameters().get_id_prefix() + i); - - INSTANCES.put(j, result); - } - - return result; - } - - public static void write_predicates () - { - for (final String id: INSTANCES.values()) - { - OUTPUT_FILE.write("(add_element instance "); - OUTPUT_FILE.write(id); - OUTPUT_FILE.write(")"); - - OUTPUT_FILE.insert_newline(); - } - } -} diff --git a/instance-calculator/src/Main.java b/instance-calculator/src/Main.java index a23da06..6fc950f 100644 --- a/instance-calculator/src/Main.java +++ b/instance-calculator/src/Main.java @@ -37,7 +37,6 @@ public class Main } create_instances(); - Instances.write_predicates(); OutputFile.close_all(); } diff --git a/instance-calculator/src/VHDLProcess.java b/instance-calculator/src/VHDLProcess.java index eba5e46..07bac2e 100644 --- a/instance-calculator/src/VHDLProcess.java +++ b/instance-calculator/src/VHDLProcess.java @@ -102,7 +102,6 @@ public class VHDLProcess result = new VHDLProcess.Instance ( - Instances.get_id_for(instances_count), this, visibility, iwfm_map @@ -115,6 +114,13 @@ public class VHDLProcess public static class Instance { + private static int instances_count; + + static + { + instances_count = 0; + } + private final String id; private final VHDLProcess parent; private final Map iwfm_map; @@ -122,13 +128,18 @@ public class VHDLProcess private Instance ( - final String id, final VHDLProcess parent, final VHDLEntity visibility, final Map iwfm_map ) { - this.id = id; + this.id = + ( + Main.get_parameters().get_id_prefix() + + "ps_" + + instances_count + ); + this.parent = parent; this.visibility = visibility; this.iwfm_map = iwfm_map; @@ -168,7 +179,6 @@ public class VHDLProcess result = new VHDLProcess.Instance ( - Instances.get_id_for(parent.instances_count), parent, visibility, new_iwfm_map @@ -187,7 +197,12 @@ public class VHDLProcess try { - of.write("(is_process_instance "); + of.write("(add_element ps_instance "); + of.write(id); + of.write(")"); + of.insert_newline(); + + of.write("(is_ps_instance_of "); of.write(id); of.write(" "); of.write(parent.get_id()); @@ -197,8 +212,6 @@ public class VHDLProcess of.write("(is_visible_in "); of.write(id); of.write(" "); - of.write(parent.get_id()); - of.write(" "); of.write(visibility.get_id()); of.write(")"); of.insert_newline(); @@ -212,12 +225,8 @@ public class VHDLProcess of.write("(process_instance_maps "); of.write(id); of.write(" "); - of.write(parent.get_id()); - of.write(" "); of.write(iwfm.getKey().get_id()); of.write(" "); - of.write(iwfm.getKey().get_parent().get_id()); - of.write(" "); of.write(iwfm.getValue().get_id()); of.write(")"); of.insert_newline(); diff --git a/instance-calculator/src/VHDLWaveform.java b/instance-calculator/src/VHDLWaveform.java index 74edc88..89cf945 100644 --- a/instance-calculator/src/VHDLWaveform.java +++ b/instance-calculator/src/VHDLWaveform.java @@ -74,7 +74,6 @@ public class VHDLWaveform result = new VHDLWaveform.Instance ( - Instances.get_id_for(instances_count), this, visibility ); @@ -104,18 +103,32 @@ public class VHDLWaveform public static class Instance { + private static int instances_count; + + static + { + instances_count = 0; + } + private final String id; private final VHDLWaveform parent; private final VHDLEntity visibility; private Instance ( - final String id, final VHDLWaveform parent, final VHDLEntity visibility ) { - this.id = id; + this.id = + ( + Main.get_parameters().get_id_prefix() + + "wfm_" + + instances_count + ); + + instances_count += 1; + this.parent = parent; this.visibility = visibility; } @@ -134,7 +147,12 @@ public class VHDLWaveform { try { - of.write("(is_waveform_instance "); + of.write("(add_element wfm_instance "); + of.write(id); + of.write(")"); + of.insert_newline(); + + of.write("(is_wfm_instance_of "); of.write(id); of.write(" "); of.write(parent.get_id()); @@ -144,8 +162,6 @@ public class VHDLWaveform of.write("(is_visible_in "); of.write(id); of.write(" "); - of.write(parent.get_id()); - of.write(" "); of.write(visibility.get_id()); of.write(")"); of.insert_newline(); @@ -166,7 +182,7 @@ public class VHDLWaveform @Override public String toString () { - return "<" + parent.get_id() + ", " + id + ">"; + return id; } } } diff --git a/instr-to-kodkod/Makefile b/instr-to-kodkod/Makefile index 8543ee4..1a36fae 100644 --- a/instr-to-kodkod/Makefile +++ b/instr-to-kodkod/Makefile @@ -96,8 +96,7 @@ MODEL_FILES = \ $(MODEL_DIR)/depths.mod \ $(MODEL_DIR)/string_to_instr.map \ $(wildcard $(MODEL_DIR)/cfg_*.mod) \ - $(MODEL_INSTANCES_DIR)/instances.mod \ - $(wildcard $(MODEL_INSTANCESDIR)/instances_in_*.mod) + $(wildcard $(MODEL_INSTANCES_DIR)/*.mod) PARSER_SOURCES = $(wildcard parser/*.g4) PARSER_CLASSES = $(PARSER_SOURCES:.g4=.class) -- cgit v1.2.3-70-g09d2 From dcc5284790f16566c4885f9e0fa3c6fb9577c11d Mon Sep 17 00:00:00 2001 From: Nathanael Sensfelder Date: Wed, 30 Aug 2017 15:26:56 +0200 Subject: Forgot to increase instances_count. --- instance-calculator/src/VHDLProcess.java | 2 ++ 1 file changed, 2 insertions(+) diff --git a/instance-calculator/src/VHDLProcess.java b/instance-calculator/src/VHDLProcess.java index 07bac2e..ff5d32c 100644 --- a/instance-calculator/src/VHDLProcess.java +++ b/instance-calculator/src/VHDLProcess.java @@ -140,6 +140,8 @@ public class VHDLProcess + instances_count ); + instances_count += 1; + this.parent = parent; this.visibility = visibility; this.iwfm_map = iwfm_map; -- cgit v1.2.3-70-g09d2 From 3466690e0a13a145d8d1eef89eba3f962f9f6e2b Mon Sep 17 00:00:00 2001 From: Nathanael Sensfelder Date: Fri, 1 Sep 2017 15:58:25 +0200 Subject: Adds test cases for the issue. --- Makefile | 2 +- data/property/simple_flip_flop.pro | 1 + data/property/simple_flip_flop_instance.pp | 6 -- data/property/simple_flip_flop_instance.pro | 95 ----------------------------- data/property/test-case/fast.pp | 6 ++ data/property/test-case/fast.pro | 57 +++++++++++++++++ data/property/test-case/slow.pp | 6 ++ data/property/test-case/slow.pro | 60 ++++++++++++++++++ 8 files changed, 131 insertions(+), 102 deletions(-) delete mode 100644 data/property/simple_flip_flop_instance.pp delete mode 100644 data/property/simple_flip_flop_instance.pro create mode 100644 data/property/test-case/fast.pp create mode 100644 data/property/test-case/fast.pro create mode 100644 data/property/test-case/slow.pp create mode 100644 data/property/test-case/slow.pro diff --git a/Makefile b/Makefile index 116e4ec..c5a5601 100644 --- a/Makefile +++ b/Makefile @@ -1,7 +1,7 @@ ## Makefile Parameters ######################################################### LEVEL_FILES = $(wildcard ${CURDIR}/data/level/*.lvl) PROPERTY_FILES = \ - $(wildcard ${CURDIR}/data/property/*.pro) + $(wildcard ${CURDIR}/data/property/test-case/*.pro) # $(wildcard ${CURDIR}/data/property/cnes/*.pro) AST_FILE = ${CURDIR}/data/ast/best_chronometer_ever.xml #AST_FILE = ${CURDIR}/data/ast/pong.xml diff --git a/data/property/simple_flip_flop.pro b/data/property/simple_flip_flop.pro index e1621c1..b054c7f 100644 --- a/data/property/simple_flip_flop.pro +++ b/data/property/simple_flip_flop.pro @@ -5,6 +5,7 @@ (ps process STRUCT_SIMPLE_FLIP_FLOP_PROCESS) ) (and + (not (eq clk reg)) (is_explicit_process ps) (is_in_sensitivity_list clk ps) (CTL_verifies ps diff --git a/data/property/simple_flip_flop_instance.pp b/data/property/simple_flip_flop_instance.pp deleted file mode 100644 index b460eec..0000000 --- a/data/property/simple_flip_flop_instance.pp +++ /dev/null @@ -1,6 +0,0 @@ -The component described by the entity $ent.IDENTIFIER$ (declared in $ent.FILE$, -line $ent.LINE$, column $ent.COLUMN$) has a simple flip-flop described by the -process $ps.LABEL$ (declared in $ps.FILE$, l. $ps.LINE$, c. $ps.COLUMN$), -controlled by $clk.IDENTIFIER$ (declared in $clk.FILE$, l. $clk.LINE$, -c. $clk.COLUMN$), and with output $reg.IDENTIFIER$ (declared in $reg.FILE$, -l. $reg.LINE$, c. $reg.COLUMN$). diff --git a/data/property/simple_flip_flop_instance.pro b/data/property/simple_flip_flop_instance.pro deleted file mode 100644 index a3881aa..0000000 --- a/data/property/simple_flip_flop_instance.pro +++ /dev/null @@ -1,95 +0,0 @@ -(tag_existing - ( - (ent entity STRUCT_ENTITY) - (reg waveform STRUCT_SIMPLE_FLIP_FLOP_OUTPUT) - (clk waveform STRUCT_SIMPLE_FLIP_FLOP_CLOCK) - (ps process STRUCT_SIMPLE_FLIP_FLOP_PROCESS) - ) - (and - (is_explicit_process ps) -;; debt: )) -;; Get ps instance -(exists i_ps ps_instance - (and - (is_visible_in i_ps ent) - (is_ps_instance_of i_ps ps) -;; debt: )) )) -;; Get a local waveform matching a clk instance -(exists i_clk wfm_instance - (and - (process_instance_maps i_ps i_clk _) -;; (is_visible_in i_clk ent) - (is_wfm_instance_of i_clk clk) - (exists local_clk waveform - (and - (process_instance_maps i_ps i_clk local_clk) - (is_in_sensitivity_list local_clk ps) -;; debt: )))) )))) -;; Get a local waveform matching a reg instance -(exists i_reg wfm_instance - (and - (process_instance_maps i_ps i_reg _) -;; (is_visible_in i_reg ent) - (is_wfm_instance_of i_reg reg) - (exists local_reg waveform - (and - (process_instance_maps i_ps i_reg local_reg) -;; debt: )))) )))))))) -;; Analyze ps using the local waveforms -(CTL_verifies ps - (AF - (and - (kind "if") - (or - (and - (is_read_structure "(??)") - (or - (is_read_element "0" "falling_edge") - (is_read_element "0" "rising_edge") - ) - (is_read_element "1" local_clk) - ) - (and - (is_read_structure "(?(??)(???))") - (is_read_element "0" "and") - (is_read_element "1" "event") - (is_read_element "2" local_clk) - (is_read_element "3" "=") - (or - (is_read_element "4" local_clk) - (is_read_element "5" local_clk) - ) - ) - (and - (is_read_structure "(?(???)(??))") - (is_read_element "0" "and") - (is_read_element "1" "=") - (or - (is_read_element "2" local_clk) - (is_read_element "3" local_clk) - ) - (is_read_element "4" "event") - (is_read_element "5" local_clk) - ) - ) - (EX - (and - (has_option "COND_WAS_TRUE") - (does_not_reach_parent_before - (and - (expr_writes local_reg) - (AX - (not - (EF - (expr_writes local_reg) - ) - ) - ) - ) - ) - ) - ) - ) - ) -) -)))))))))))) diff --git a/data/property/test-case/fast.pp b/data/property/test-case/fast.pp new file mode 100644 index 0000000..b460eec --- /dev/null +++ b/data/property/test-case/fast.pp @@ -0,0 +1,6 @@ +The component described by the entity $ent.IDENTIFIER$ (declared in $ent.FILE$, +line $ent.LINE$, column $ent.COLUMN$) has a simple flip-flop described by the +process $ps.LABEL$ (declared in $ps.FILE$, l. $ps.LINE$, c. $ps.COLUMN$), +controlled by $clk.IDENTIFIER$ (declared in $clk.FILE$, l. $clk.LINE$, +c. $clk.COLUMN$), and with output $reg.IDENTIFIER$ (declared in $reg.FILE$, +l. $reg.LINE$, c. $reg.COLUMN$). diff --git a/data/property/test-case/fast.pro b/data/property/test-case/fast.pro new file mode 100644 index 0000000..10bc135 --- /dev/null +++ b/data/property/test-case/fast.pro @@ -0,0 +1,57 @@ +(tag_existing + ( + (ent entity STRUCT_ENTITY) + (reg waveform STRUCT_SIMPLE_FLIP_FLOP_OUTPUT) + (clk waveform STRUCT_SIMPLE_FLIP_FLOP_CLOCK) + (ps process STRUCT_SIMPLE_FLIP_FLOP_PROCESS) + ) + (and + (not (eq reg clk)) + (is_explicit_process ps) + ;; debt: )) + ;; Get ps instance + (exists i_ps ps_instance + (and + (is_visible_in i_ps ent) + (is_ps_instance_of i_ps ps) + ;; debt: )) )) + ;; Get a local waveform matching a clk instance + (exists i_clk wfm_instance + (and + (process_instance_maps i_ps i_clk _) + ;; (is_visible_in i_clk ent) + (is_wfm_instance_of i_clk clk) + (exists local_clk waveform + (and + (process_instance_maps i_ps i_clk local_clk) + (is_in_sensitivity_list local_clk ps) + ;; debt: )))) )))) + ;; Get a local waveform matching a reg instance + (exists i_reg wfm_instance + (and + (process_instance_maps i_ps i_reg _) + ;; (is_visible_in i_reg ent) + (is_wfm_instance_of i_reg reg) + (exists local_reg waveform + (and + (process_instance_maps i_ps i_reg local_reg) + ;; debt: )))) )))))))) + ;; Analyze ps using the local waveforms + (CTL_verifies ps + (AF + ;; using local_clk or local_reg here makes the property take forever to verify.... + (kind "if") + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) +) diff --git a/data/property/test-case/slow.pp b/data/property/test-case/slow.pp new file mode 100644 index 0000000..b460eec --- /dev/null +++ b/data/property/test-case/slow.pp @@ -0,0 +1,6 @@ +The component described by the entity $ent.IDENTIFIER$ (declared in $ent.FILE$, +line $ent.LINE$, column $ent.COLUMN$) has a simple flip-flop described by the +process $ps.LABEL$ (declared in $ps.FILE$, l. $ps.LINE$, c. $ps.COLUMN$), +controlled by $clk.IDENTIFIER$ (declared in $clk.FILE$, l. $clk.LINE$, +c. $clk.COLUMN$), and with output $reg.IDENTIFIER$ (declared in $reg.FILE$, +l. $reg.LINE$, c. $reg.COLUMN$). diff --git a/data/property/test-case/slow.pro b/data/property/test-case/slow.pro new file mode 100644 index 0000000..2566a6f --- /dev/null +++ b/data/property/test-case/slow.pro @@ -0,0 +1,60 @@ +(tag_existing + ( + (ent entity STRUCT_ENTITY) + (reg waveform STRUCT_SIMPLE_FLIP_FLOP_OUTPUT) + (clk waveform STRUCT_SIMPLE_FLIP_FLOP_CLOCK) + (ps process STRUCT_SIMPLE_FLIP_FLOP_PROCESS) + ) + (and + (not (eq reg clk)) + (is_explicit_process ps) + ;; debt: )) + ;; Get ps instance + (exists i_ps ps_instance + (and + (is_visible_in i_ps ent) + (is_ps_instance_of i_ps ps) + ;; debt: )) )) + ;; Get a local waveform matching a clk instance + (exists i_clk wfm_instance + (and + (process_instance_maps i_ps i_clk _) + ;; (is_visible_in i_clk ent) + (is_wfm_instance_of i_clk clk) + (exists local_clk waveform + (and + (process_instance_maps i_ps i_clk local_clk) + (is_in_sensitivity_list local_clk ps) + ;; debt: )))) )))) + ;; Get a local waveform matching a reg instance + (exists i_reg wfm_instance + (and + (process_instance_maps i_ps i_reg _) + ;; (is_visible_in i_reg ent) + (is_wfm_instance_of i_reg reg) + (exists local_reg waveform + (and + (process_instance_maps i_ps i_reg local_reg) + ;; debt: )))) )))))))) + ;; Analyze ps using the local waveforms + (CTL_verifies ps + (AF + ;; using local_clk or local_reg here makes the property take forever to verify.... + (and + (kind "if") + (is_read_element "1" local_clk) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) +) -- cgit v1.2.3-70-g09d2 From e90c20f7c17b73c6ae8ff1d653278144c713a0e6 Mon Sep 17 00:00:00 2001 From: Nathanael Sensfelder Date: Sat, 2 Sep 2017 14:48:32 +0200 Subject: Finer imports. --- instance-calculator/src/Main.java | 8 +++++--- instance-calculator/src/ModelFile.java | 3 ++- instance-calculator/src/QuickParser.java | 12 ++++++++---- instance-calculator/src/VHDLArchitecture.java | 7 ++++++- instance-calculator/src/VHDLComponent.java | 5 ++++- instance-calculator/src/VHDLEntity.java | 6 ++++-- instance-calculator/src/VHDLProcess.java | 7 +++++-- instance-calculator/src/VHDLWaveform.java | 6 ++++-- 8 files changed, 38 insertions(+), 16 deletions(-) diff --git a/instance-calculator/src/Main.java b/instance-calculator/src/Main.java index 6fc950f..b66a63b 100644 --- a/instance-calculator/src/Main.java +++ b/instance-calculator/src/Main.java @@ -1,7 +1,9 @@ -/* FIXME: Finer imports */ -import java.util.*; +import java.util.ArrayDeque; +import java.util.ArrayList; +import java.util.Collection; +import java.util.Deque; -import java.io.*; +import java.io.FileWriter; public class Main { diff --git a/instance-calculator/src/ModelFile.java b/instance-calculator/src/ModelFile.java index 1f9297e..be84674 100644 --- a/instance-calculator/src/ModelFile.java +++ b/instance-calculator/src/ModelFile.java @@ -1,4 +1,5 @@ -import java.io.*; +import java.io.IOException; +import java.io.FileNotFoundException; public class ModelFile { diff --git a/instance-calculator/src/QuickParser.java b/instance-calculator/src/QuickParser.java index 47cea27..383373e 100644 --- a/instance-calculator/src/QuickParser.java +++ b/instance-calculator/src/QuickParser.java @@ -1,7 +1,11 @@ -/* FIXME: Finer imports */ -import java.io.*; -import java.util.regex.*; -import java.util.*; +import java.io.BufferedReader; +import java.io.FileReader; +import java.io.IOException; +import java.io.FileNotFoundException; + +import java.util.List; +import java.util.regex.Matcher; +import java.util.regex.Pattern; public class QuickParser { diff --git a/instance-calculator/src/VHDLArchitecture.java b/instance-calculator/src/VHDLArchitecture.java index 407a09f..a3aa7ac 100644 --- a/instance-calculator/src/VHDLArchitecture.java +++ b/instance-calculator/src/VHDLArchitecture.java @@ -1,4 +1,9 @@ -import java.util.*; +import java.util.ArrayDeque; +import java.util.ArrayList; +import java.util.Collection; +import java.util.Deque; +import java.util.Map; +import java.util.HashMap; public class VHDLArchitecture { diff --git a/instance-calculator/src/VHDLComponent.java b/instance-calculator/src/VHDLComponent.java index 958a2e4..76b1dc9 100644 --- a/instance-calculator/src/VHDLComponent.java +++ b/instance-calculator/src/VHDLComponent.java @@ -1,4 +1,7 @@ -import java.util.*; +import java.util.ArrayList; +import java.util.Collection; +import java.util.Map; +import java.util.HashMap; public class VHDLComponent { diff --git a/instance-calculator/src/VHDLEntity.java b/instance-calculator/src/VHDLEntity.java index 2765229..d2a8e07 100644 --- a/instance-calculator/src/VHDLEntity.java +++ b/instance-calculator/src/VHDLEntity.java @@ -1,5 +1,7 @@ -import java.util.*; -import java.io.BufferedWriter; +import java.util.ArrayList; +import java.util.Collection; +import java.util.Map; +import java.util.HashMap; public class VHDLEntity { diff --git a/instance-calculator/src/VHDLProcess.java b/instance-calculator/src/VHDLProcess.java index ff5d32c..a4f150e 100644 --- a/instance-calculator/src/VHDLProcess.java +++ b/instance-calculator/src/VHDLProcess.java @@ -1,5 +1,8 @@ -import java.util.*; -import java.io.BufferedWriter; +import java.util.ArrayList; +import java.util.Collection; +import java.util.Map; +import java.util.HashMap; +import java.util.Set; public class VHDLProcess { diff --git a/instance-calculator/src/VHDLWaveform.java b/instance-calculator/src/VHDLWaveform.java index 89cf945..feb1e51 100644 --- a/instance-calculator/src/VHDLWaveform.java +++ b/instance-calculator/src/VHDLWaveform.java @@ -1,5 +1,7 @@ -import java.util.*; -import java.io.BufferedWriter; +import java.util.ArrayList; +import java.util.Collection; +import java.util.Map; +import java.util.HashMap; public class VHDLWaveform { -- cgit v1.2.3-70-g09d2 From 474f870ea7af014808d109fa687b5c75d8861bd1 Mon Sep 17 00:00:00 2001 From: Nathanael Sensfelder Date: Mon, 4 Sep 2017 14:27:00 +0200 Subject: Fixes jar not downloading. --- instr-to-kodkod/Makefile | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/instr-to-kodkod/Makefile b/instr-to-kodkod/Makefile index 03e451a..56c129a 100644 --- a/instr-to-kodkod/Makefile +++ b/instr-to-kodkod/Makefile @@ -106,7 +106,8 @@ compile: $(PARSER_CLASSES) $(CLASSES) model: cfg-generator -solutions: cfg-generator $(PARSER_CLASSES) $(CLASSES) $(SOLUTION_FILES) +solutions: cfg-generator $(REQUIRED_JARS) $(PARSER_CLASSES) $(CLASSES) \ + $(SOLUTION_FILES) clean: $(MAKE) -C parser clean -- cgit v1.2.3-70-g09d2 From 77838a1342b53ca97d842ef47ff91f44f6a5bbeb Mon Sep 17 00:00:00 2001 From: Nathanael Sensfelder Date: Mon, 18 Sep 2017 10:33:11 +0200 Subject: Go back to the usual default properties. --- Makefile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile index c5a5601..a959838 100644 --- a/Makefile +++ b/Makefile @@ -1,8 +1,8 @@ ## Makefile Parameters ######################################################### LEVEL_FILES = $(wildcard ${CURDIR}/data/level/*.lvl) PROPERTY_FILES = \ - $(wildcard ${CURDIR}/data/property/test-case/*.pro) -# $(wildcard ${CURDIR}/data/property/cnes/*.pro) + $(wildcard ${CURDIR}/data/property/*.pro) \ + $(wildcard ${CURDIR}/data/property/cnes/*.pro) AST_FILE = ${CURDIR}/data/ast/best_chronometer_ever.xml #AST_FILE = ${CURDIR}/data/ast/pong.xml -- cgit v1.2.3-70-g09d2