Merge branch 'instance-calculator'

21 files changed, 1925 insertions, 3 deletions

diff --git a/Makefile b/Makefile
index 19a69d8..c5a5601 100644
--- a/Makefile
+++ b/Makefile
@@ -1,17 +1,19 @@
 ## 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/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
 
 TMP_DIR = /tmp/tabellion
 MODEL_DIR = $(TMP_DIR)/mod
+MODEL_INSTANCES_DIR = $(MODEL_DIR)/instance
 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 +26,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/data/level/instances.lvl b/data/level/instances.lvl
new file mode 100644
index 0000000..ad6e93f
--- /dev/null
+++ b/data/level/instances.lvl
@@ -0,0 +1,23 @@
+;; Instances
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; TYPES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(add_type wfm_instance)
+(add_type ps_instance)
+
+;; Redundancies
+(add_type entity)
+(add_type process)
+(add_type waveform)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; PREDICATES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(add_predicate is_wfm_instance_of wfm_instance waveform)
+(add_predicate is_visible_in wfm_instance entity)
+
+(add_predicate is_ps_instance_of ps_instance process)
+(add_predicate is_visible_in ps_instance entity)
+
+(add_predicate process_instance_maps ps_instance wfm_instance waveform)
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/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)
+                                          )
+                                       )
+                                    )
+                                 )
+                              )
+                           )
+                        )
+                     )
+                  )
+               )
+            )
+         )
+      )
+   )
+)
diff --git a/instance-calculator/Makefile b/instance-calculator/Makefile
new file mode 100644
index 0000000..9dddc88
--- /dev/null
+++ b/instance-calculator/Makefile
@@ -0,0 +1,75 @@
+## Parameters ##################################################################
+#### Where to find the model
+ifndef MODEL_DIR
+MODEL_DIR =
+endif
+
+#### Where to store the Instance model
+ifndef MODEL_INSTANCES_DIR
+MODEL_INSTANCES_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 $(MODEL_INSTANCES_DIR)),)
+$(error No MODEL_INSTANCES_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_FILE = $(MODEL_DIR)/structural.mod
+OUTPUT_FILE = $(MODEL_INSTANCES_DIR)/witness
+
+## Makefile Rules ##############################################################
+compile: $(CLASSES)
+
+model: $(CLASSES) $(MODEL_INSTANCES_DIR) $(OUTPUT_FILE)
+
+solutions:
+
+clean:
+	rm -f $(CLASSES)
+	rm -f $(MODEL_INSTANCES_DIR)/*
+
+clean_model:
+	rm -f $(MODEL_INSTANCES_DIR)/*
+
+clean_solutions:
+
+########
+%.class: %.java
+	$(JAVAC) -cp $(CLASSPATH) $<
+
+$(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/.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/Main.java b/instance-calculator/src/Main.java
new file mode 100644
index 0000000..b66a63b
--- /dev/null
+++ b/instance-calculator/src/Main.java
@@ -0,0 +1,121 @@
+import java.util.ArrayDeque;
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.Deque;
+
+import java.io.FileWriter;
+
+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;
+      }
+
+      create_instances();
+      OutputFile.close_all();
+   }
+
+   private static void create_instances ()
+   {
+      final Collection<VHDLEntity> futur_candidates;
+      final Deque<VHDLEntity> candidates;
+      final Collection<VHDLEntity> processed_candidates;
+      boolean is_stuck;
+
+      futur_candidates = new ArrayList<VHDLEntity>();
+      candidates = new ArrayDeque<VHDLEntity>();
+      processed_candidates = new ArrayList<VHDLEntity>();
+
+      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();
+
+               e.write_predicates();
+               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 ()
+   {
+      return PARAMETERS;
+   }
+}
diff --git a/instance-calculator/src/ModelFile.java b/instance-calculator/src/ModelFile.java
new file mode 100644
index 0000000..be84674
--- /dev/null
+++ b/instance-calculator/src/ModelFile.java
@@ -0,0 +1,310 @@
+import java.io.IOException;
+import java.io.FileNotFoundException;
+
+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;
+         }
+      }
+
+      VHDLArchitecture.resolve_all_waveforms();
+
+      return true;
+   }
+
+   private static boolean handle_add_element
+   (
+      final String[] input
+   )
+   {
+      if (input.length != 3)
+      {
+         return false;
+      }
+
+      if (input[1].equals("entity"))
+      {
+         VHDLEntity.add_element(input[2]);
+      }
+      else if (input[1].equals("architecture"))
+      {
+         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]);
+      }
+      else if (input[1].equals("component"))
+      {
+         VHDLComponent.add_element(input[2]);
+      }
+
+      return true;
+   }
+
+   private static boolean handle_is_accessed_by
+   (
+      final String[] input
+   )
+   {
+      final VHDLProcess ps;
+      final VHDLWaveform wfm;
+
+      if (input.length != 3)
+      {
+         return false;
+      }
+
+      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
+   (
+      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.get_from_id(input[2]).add_port(input[1]);
+
+      return true;
+   }
+
+   private static boolean handle_is_architecture_of
+   (
+      final String[] input
+   )
+   {
+      final VHDLEntity e;
+      final VHDLArchitecture arch;
+
+      if (input.length != 3)
+      {
+         return false;
+      }
+
+      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
+   (
+      final String[] input
+   )
+   {
+      final VHDLArchitecture arch;
+      final VHDLProcess ps;
+      final VHDLComponent cmp;
+
+      if (input.length != 3)
+      {
+         return false;
+      }
+
+      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;
+      }
+
+      arch.add_futur_waveform(input[1]);
+
+      return true;
+   }
+
+   private static boolean handle_is_component_of
+   (
+      final String[] input
+   )
+   {
+      if (input.length != 3)
+      {
+         return false;
+      }
+
+      VHDLComponent.get_from_id(input[1]).set_destination
+      (
+         VHDLEntity.get_from_id(input[2])
+      );
+
+      return true;
+   }
+
+   private static boolean handle_port_maps
+   (
+      final String[] input
+   )
+   {
+      if (input.length != 4)
+      {
+         return false;
+      }
+
+      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/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<OutputFile> ALL_OUTPUT_FILES;
+
+   static
+   {
+      ALL_OUTPUT_FILES = new ArrayList<OutputFile>();
+   }
+
+   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
new file mode 100644
index 0000000..b8bba30
--- /dev/null
+++ b/instance-calculator/src/Parameters.java
@@ -0,0 +1,64 @@
+public class Parameters
+{
+   private final String model_file;
+   private final String id_prefix;
+   private final String output_dir;
+   private final boolean are_valid;
+
+   public static void print_usage ()
+   {
+      System.out.println
+      (
+         "Instance-Calculator\n"
+         + "USAGE:\n"
+         + "\tjava Main <INSTRUCTIONS> <ID_PREFIX> <OUTPUT_DIR>\n"
+         + "PARAMETERS:\n"
+         + "\t<INSTRUCTIONS>\tInstruction file describing the model.\n"
+         + "\t<ID_PREFIX>\tPrefix for the IDs of generated paths.\n"
+         + "\t<OUTPUT_DIR>\tDirectory in which to output the generated"
+         + " instruction files."
+      );
+   }
+
+   public Parameters (final String... args)
+   {
+      if (args.length != 3)
+      {
+         print_usage();
+
+         model_file = new String();
+         id_prefix = new String();
+         output_dir = new String();
+
+         are_valid = false;
+      }
+      else
+      {
+         model_file = args[0];
+         id_prefix = args[1];
+         output_dir = args[2];
+
+         are_valid = true;
+      }
+   }
+
+   public String get_model_file ()
+   {
+      return model_file;
+   }
+
+   public String get_id_prefix ()
+   {
+      return id_prefix;
+   }
+
+   public String get_output_directory ()
+   {
+      return output_dir;
+   }
+
+   public boolean are_valid ()
+   {
+      return are_valid;
+   }
+}
diff --git a/instance-calculator/src/QuickParser.java b/instance-calculator/src/QuickParser.java
new file mode 100644
index 0000000..383373e
--- /dev/null
+++ b/instance-calculator/src/QuickParser.java
@@ -0,0 +1,62 @@
+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
+{
+   private static final Pattern instr_pattern;
+   private final BufferedReader buffered_reader;
+
+   static
+   {
+      instr_pattern = Pattern.compile("\\((?<list>[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<String> 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
new file mode 100644
index 0000000..a3aa7ac
--- /dev/null
+++ b/instance-calculator/src/VHDLArchitecture.java
@@ -0,0 +1,179 @@
+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
+{
+   private static final Map<String, VHDLArchitecture> FROM_ID;
+
+   static
+   {
+      FROM_ID = new HashMap<String, VHDLArchitecture>();
+   }
+
+   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))
+      {
+         FROM_ID.put(id, new VHDLArchitecture(id));
+      }
+   }
+
+   public static VHDLArchitecture get_from_id (final String id)
+   {
+      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 VHDLArchitecture find (final String id)
+   {
+      return FROM_ID.get(id);
+   }
+
+/******************************************************************************/
+   private final Collection<VHDLProcess> processes;
+   private final Collection<VHDLComponent> components;
+   private final Collection<VHDLWaveform> waveforms;
+   private final Deque<String> futur_waveforms;
+   private final String id;
+
+   private VHDLEntity entity;
+
+   private VHDLArchitecture (final String id)
+   {
+      this.id = id;
+
+      processes = new ArrayList<VHDLProcess>();
+      components = new ArrayList<VHDLComponent>();
+      waveforms = new ArrayList<VHDLWaveform>();
+      futur_waveforms = new ArrayDeque<String>();
+   }
+
+   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 Collection<VHDLComponent> get_components ()
+   {
+      return components;
+   }
+
+   public void add_waveform (final VHDLWaveform wfm)
+   {
+      if (!waveforms.contains(wfm))
+      {
+         waveforms.add(wfm);
+      }
+   }
+
+   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<VHDLProcess.Instance> process_instances,
+      final Collection<VHDLWaveform.Instance> waveform_instances,
+      final Map<VHDLWaveform, VHDLWaveform.Instance> 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
new file mode 100644
index 0000000..76b1dc9
--- /dev/null
+++ b/instance-calculator/src/VHDLComponent.java
@@ -0,0 +1,146 @@
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.Map;
+import java.util.HashMap;
+
+public class VHDLComponent
+{
+   private static final Map<String, VHDLComponent> FROM_ID;
+
+   static
+   {
+      FROM_ID = new HashMap<String, VHDLComponent>();
+   }
+
+   public static void add_element (final String id)
+   {
+      if (!FROM_ID.containsKey(id))
+      {
+         FROM_ID.put(id, new VHDLComponent(id));
+      }
+   }
+
+   public static VHDLComponent get_from_id (final String id)
+   {
+      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 VHDLComponent find (final String id)
+   {
+      return FROM_ID.get(id);
+   }
+
+/******************************************************************************/
+   private final Map<String, String> reverse_port_map;
+   private final String id;
+
+   private VHDLEntity destination;
+   private VHDLArchitecture parent;
+
+   public void set_destination (final VHDLEntity dest)
+   {
+      destination = dest;
+   }
+
+   public VHDLEntity get_destination ()
+   {
+      return destination;
+   }
+
+   public void set_architecture (final VHDLArchitecture arch)
+   {
+      parent = arch;
+   }
+
+   public void add_port_map (final String src, final String dest)
+   {
+      reverse_port_map.put(dest, src);
+   }
+
+   public void add_instance_content_to
+   (
+      final Collection<VHDLProcess.Instance> process_instances,
+      final Collection<VHDLWaveform.Instance> waveform_instances,
+      final Map<VHDLWaveform, VHDLWaveform.Instance> local_conversion
+   )
+   {
+      final Collection<VHDLProcess.Instance> dest_process_instances;
+      final Collection<VHDLWaveform.Instance> dest_waveform_instances;
+      final Map<VHDLWaveform.Instance, VHDLWaveform.Instance> wfm_map;
+
+      dest_process_instances = destination.get_process_instances();
+      dest_waveform_instances = destination.get_waveform_instances();
+
+      wfm_map = new HashMap<VHDLWaveform.Instance, VHDLWaveform.Instance>();
+
+      for (final VHDLWaveform.Instance i_wfm: dest_waveform_instances)
+      {
+         final String src_wfm, dest_port;
+         final VHDLWaveform.Instance replacement;
+
+         dest_port =
+            Waveforms.get_id_from_waveform_id
+            (
+               i_wfm.get_parent().get_id()
+            );
+
+         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
+               (
+                  VHDLWaveform.get_from_id
+                  (
+                     src_wfm
+                  )
+               );
+         }
+
+         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;
+
+      reverse_port_map = new HashMap<String, String>();
+   }
+}
diff --git a/instance-calculator/src/VHDLEntity.java b/instance-calculator/src/VHDLEntity.java
new file mode 100644
index 0000000..d2a8e07
--- /dev/null
+++ b/instance-calculator/src/VHDLEntity.java
@@ -0,0 +1,150 @@
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.Map;
+import java.util.HashMap;
+
+public class VHDLEntity
+{
+   private static final Map<String, VHDLEntity> FROM_ID;
+
+   static
+   {
+      FROM_ID = new HashMap<String, VHDLEntity>();
+   }
+
+   public static Collection<VHDLEntity> get_all ()
+   {
+      return FROM_ID.values();
+   }
+
+   public static void add_element (final String id)
+   {
+      if (!FROM_ID.containsKey(id))
+      {
+         FROM_ID.put(id, new VHDLEntity(id));
+      }
+   }
+
+   public static VHDLEntity get_from_id (final String id)
+   {
+      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 VHDLEntity find (final String id)
+   {
+      return FROM_ID.get(id);
+   }
+
+/******************************************************************************/
+   private final Collection<VHDLProcess.Instance> process_instances;
+   private final Collection<VHDLWaveform.Instance> waveform_instances;
+
+   private final OutputFile output_file;
+   private final Collection<String> ports;
+   private final String id;
+
+   private VHDLArchitecture architecture;
+
+   private VHDLEntity (final String id)
+   {
+      this.id = id;
+      ports = new ArrayList<String>();
+
+      architecture = null;
+
+      this.process_instances = new ArrayList<VHDLProcess.Instance>();
+      this.waveform_instances = new ArrayList<VHDLWaveform.Instance>();
+
+      output_file = OutputFile.new_output_file("instances_in_" + id + ".mod");
+   }
+
+   public String get_id ()
+   {
+      return id;
+   }
+
+   public void add_port (final String pt)
+   {
+      if (!ports.contains(pt))
+      {
+         ports.add(pt);
+      }
+   }
+
+   public void set_architecture (final VHDLArchitecture arch)
+   {
+      architecture = arch;
+   }
+
+   public VHDLArchitecture get_architecture ()
+   {
+      return architecture;
+   }
+
+   public Collection<VHDLProcess.Instance> get_process_instances ()
+   {
+      return process_instances;
+   }
+
+   public Collection<VHDLWaveform.Instance> get_waveform_instances ()
+   {
+      return waveform_instances;
+   }
+
+   public void generate_instance ()
+   {
+      final Map<VHDLWaveform, VHDLWaveform.Instance> local_conversion;
+
+      local_conversion = new HashMap<VHDLWaveform, VHDLWaveform.Instance>();
+
+      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
+      );
+   }
+
+   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
new file mode 100644
index 0000000..a4f150e
--- /dev/null
+++ b/instance-calculator/src/VHDLProcess.java
@@ -0,0 +1,253 @@
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.Map;
+import java.util.HashMap;
+import java.util.Set;
+
+public class VHDLProcess
+{
+   private static final Map<String, VHDLProcess> FROM_ID;
+
+   static
+   {
+      FROM_ID = new HashMap<String, VHDLProcess>();
+   }
+
+   public static void add_element (final String id)
+   {
+      if (!FROM_ID.containsKey(id))
+      {
+         FROM_ID.put(id, new VHDLProcess(id));
+      }
+   }
+
+   public static VHDLProcess get_from_id (final String id)
+   {
+      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);
+   }
+
+/******************************************************************************/
+   private final Collection<VHDLWaveform> accessed_wfm;
+   private final Collection<VHDLProcess.Instance> instances;
+   private final String id;
+   private int instances_count;
+
+   private VHDLArchitecture architecture;
+
+   private VHDLProcess (final String id)
+   {
+      this.id = id;
+      accessed_wfm = new ArrayList<VHDLWaveform>();
+      instances = new ArrayList<VHDLProcess.Instance>();
+      instances_count = 0;
+      architecture = null;
+   }
+
+   public String get_id ()
+   {
+      return id;
+   }
+
+   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 VHDLProcess.Instance generate_base_instance
+   (
+      final VHDLEntity visibility,
+      final Collection<VHDLWaveform.Instance> waveform_instances
+   )
+   {
+      final VHDLProcess.Instance result;
+      final Map<VHDLWaveform.Instance, VHDLWaveform> iwfm_map;
+
+      iwfm_map = new HashMap<VHDLWaveform.Instance, VHDLWaveform>();
+
+      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
+         (
+            this,
+            visibility,
+            iwfm_map
+         );
+
+      instances_count += 1;
+
+      return result;
+   }
+
+   public static class Instance
+   {
+      private static int instances_count;
+
+      static
+      {
+         instances_count = 0;
+      }
+
+      private final String id;
+      private final VHDLProcess parent;
+      private final Map<VHDLWaveform.Instance, VHDLWaveform> iwfm_map;
+      private final VHDLEntity visibility;
+
+      private Instance
+      (
+         final VHDLProcess parent,
+         final VHDLEntity visibility,
+         final Map<VHDLWaveform.Instance, VHDLWaveform> iwfm_map
+      )
+      {
+         this.id =
+            (
+               Main.get_parameters().get_id_prefix()
+               + "ps_"
+               + instances_count
+            );
+
+         instances_count += 1;
+
+         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<VHDLWaveform.Instance, VHDLWaveform.Instance> convertion
+      )
+      {
+         final VHDLProcess.Instance result;
+         final Set<Map.Entry<VHDLWaveform.Instance, VHDLWaveform>> iwfm_set;
+         final Map<VHDLWaveform.Instance, VHDLWaveform> new_iwfm_map;
+
+         iwfm_set = iwfm_map.entrySet();
+
+         new_iwfm_map = new HashMap<VHDLWaveform.Instance, VHDLWaveform>();
+
+         for
+         (
+            final Map.Entry<VHDLWaveform.Instance, VHDLWaveform> me: iwfm_set
+         )
+         {
+            new_iwfm_map.put
+            (
+               convertion.get(me.getKey()),
+               me.getValue()
+            );
+         }
+
+         result =
+            new VHDLProcess.Instance
+            (
+               parent,
+               visibility,
+               new_iwfm_map
+            );
+
+         parent.instances_count += 1;
+
+         return result;
+      }
+
+      public void write_predicates_to (final OutputFile of)
+      {
+         final Set<Map.Entry<VHDLWaveform.Instance, VHDLWaveform>> iwfm_set;
+
+         iwfm_set = iwfm_map.entrySet();
+
+         try
+         {
+            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());
+            of.write(")");
+            of.insert_newline();
+
+            of.write("(is_visible_in ");
+            of.write(id);
+            of.write(" ");
+            of.write(visibility.get_id());
+            of.write(")");
+            of.insert_newline();
+
+            for
+            (
+               final Map.Entry<VHDLWaveform.Instance, VHDLWaveform> iwfm:
+               iwfm_set
+            )
+            {
+               of.write("(process_instance_maps ");
+               of.write(id);
+               of.write(" ");
+               of.write(iwfm.getKey().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
new file mode 100644
index 0000000..feb1e51
--- /dev/null
+++ b/instance-calculator/src/VHDLWaveform.java
@@ -0,0 +1,190 @@
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.Map;
+import java.util.HashMap;
+
+public class VHDLWaveform
+{
+   private static final Map<String, VHDLWaveform> FROM_ID;
+
+   static
+   {
+      FROM_ID = new HashMap<String, VHDLWaveform>();
+   }
+
+   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)
+   {
+      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."
+         );
+
+         new Exception().printStackTrace();
+
+         System.exit(-1);
+      }
+
+      return result;
+   }
+
+   public static VHDLWaveform find (final String id)
+   {
+      return FROM_ID.get(id);
+   }
+
+/******************************************************************************/
+   private final Collection<String> accessed_wfm;
+   private final Collection<VHDLWaveform.Instance> instances;
+   private final String id;
+   private int instances_count;
+
+   private VHDLArchitecture architecture;
+
+   private VHDLWaveform (final String id)
+   {
+      this.id = id;
+      accessed_wfm = new ArrayList<String>();
+      instances = new ArrayList<VHDLWaveform.Instance>();
+      instances_count = 0;
+      architecture = null;
+   }
+
+   public VHDLWaveform.Instance add_instance
+   (
+      final VHDLEntity visibility
+   )
+   {
+      final VHDLWaveform.Instance result;
+
+      result =
+         new VHDLWaveform.Instance
+         (
+            this,
+            visibility
+         );
+
+      instances.add(result);
+
+      instances_count += 1;
+
+      return result;
+   }
+
+   public String get_id ()
+   {
+      return id;
+   }
+
+   public void set_architecture (final VHDLArchitecture arch)
+   {
+      architecture = arch;
+   }
+
+   @Override
+   public String toString ()
+   {
+      return id;
+   }
+
+   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 VHDLWaveform parent,
+         final VHDLEntity visibility
+      )
+      {
+         this.id =
+            (
+               Main.get_parameters().get_id_prefix()
+               + "wfm_"
+               + instances_count
+            );
+
+         instances_count += 1;
+
+         this.parent = parent;
+         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("(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());
+            of.write(")");
+            of.insert_newline();
+
+            of.write("(is_visible_in ");
+            of.write(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 id;
+      }
+   }
+}
diff --git a/instance-calculator/src/Waveforms.java b/instance-calculator/src/Waveforms.java
new file mode 100644
index 0000000..9492d16
--- /dev/null
+++ b/instance-calculator/src/Waveforms.java
@@ -0,0 +1,74 @@
+import java.util.Map;
+import java.util.HashMap;
+
+public class Waveforms
+{
+   private static final Map<String, String> FROM_WAVEFORM;
+   private static final Map<String, String> TO_WAVEFORM;
+
+   static
+   {
+      FROM_WAVEFORM = new HashMap<String, String>();
+      TO_WAVEFORM = new HashMap<String, String>();
+   }
+
+   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;
+   }
+
+   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);
+   }
+}
diff --git a/instr-to-kodkod/Makefile b/instr-to-kodkod/Makefile
index 56c129a..08af039 100644
--- a/instr-to-kodkod/Makefile
+++ b/instr-to-kodkod/Makefile
@@ -95,7 +95,8 @@ 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) \
+	$(wildcard $(MODEL_INSTANCES_DIR)/*.mod)
 PARSER_SOURCES = $(wildcard parser/*.g4)
 PARSER_CLASSES = $(PARSER_SOURCES:.g4=.class)