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.

10 files changed, 157 insertions, 75 deletions

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)