From ee9d405bc917be3f596ccd2ffd2d7ddc01687d31 Mon Sep 17 00:00:00 2001
From: Nathanael Sensfelder <SpamShield0@MultiAgentSystems.org>
Date: Mon, 28 Aug 2017 16:27:12 +0200
Subject: Starts the Instance Calculator

---
 instance-calculator/Makefile | 69 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 69 insertions(+)
 create mode 100644 instance-calculator/Makefile

(limited to 'instance-calculator/Makefile')

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)
+
-- 
cgit v1.2.3-70-g09d2


From ea11fdc81ed7a8df14868476c04bf2fe7c7b6393 Mon Sep 17 00:00:00 2001
From: Nathanael Sensfelder <SpamShield0@MultiAgentSystems.org>
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(-)

(limited to 'instance-calculator/Makefile')

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<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();
+
+               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<VHDLComponent> 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<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))
@@ -64,6 +69,11 @@ public class VHDLEntity
       this.waveform_instances = new ArrayList<VHDLWaveform.Instance>();
    }
 
+   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<VHDLProcess.Instance> 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 aebd8f1bd52495b0a787e0cccfa4501141eace2b Mon Sep 17 00:00:00 2001
From: Nathanael Sensfelder <SpamShield0@MultiAgentSystems.org>
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

(limited to 'instance-calculator/Makefile')

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<Integer, String> instances;
+   private static final Map<Integer, String> INSTANCES;
+   private static final OutputFile OUTPUT_FILE;
 
    static
    {
-      instances = new HashMap<Integer, String>();
+      INSTANCES = new HashMap<Integer, String>();
+      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<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
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 <INSTRUCTIONS> <ID_PREFIX> <OUTPUT_FILE>\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_FILE>\tFile in which to output the generated"
-         + " instructions."
+         + "\t<OUTPUT_DIR>\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<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))
@@ -48,6 +56,7 @@ public class VHDLArchitecture
    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;
@@ -59,6 +68,7 @@ public class VHDLArchitecture
       processes = new ArrayList<VHDLProcess>();
       components = new ArrayList<VHDLComponent>();
       waveforms = new ArrayList<VHDLWaveform>();
+      futur_waveforms = new ArrayDeque<String>();
    }
 
    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<VHDLProcess.Instance> 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<String, String> port_map;
+   private final Map<String, String> 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<String, String>();
+      reverse_port_map = new HashMap<String, String>();
    }
 }
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<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;
 
@@ -67,6 +69,8 @@ public class VHDLEntity
 
       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 ()
@@ -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<Map.Entry<VHDLWaveform.Instance, VHDLWaveform>> 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<VHDLWaveform.Instance, VHDLWaveform> 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 <SpamShield0@MultiAgentSystems.org>
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

(limited to 'instance-calculator/Makefile')

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 <SpamShield0@MultiAgentSystems.org>
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

(limited to 'instance-calculator/Makefile')

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<Integer, String> INSTANCES;
-   private static final OutputFile OUTPUT_FILE;
-
-   static
-   {
-      INSTANCES = new HashMap<Integer, String>();
-      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<VHDLWaveform.Instance, VHDLWaveform> iwfm_map;
@@ -122,13 +128,18 @@ public class VHDLProcess
 
       private Instance
       (
-         final String id,
          final VHDLProcess parent,
          final VHDLEntity visibility,
          final Map<VHDLWaveform.Instance, VHDLWaveform> 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