From d18ca72caf2004c7725b3de670c7397c5bf85eb4 Mon Sep 17 00:00:00 2001
From: Nathanael Sensfelder <SpamShield0@MultiAgentSystems.org>
Date: Fri, 4 Aug 2017 12:47:30 +0200
Subject: For some reason, CNE_01700 no longer works.

---
 data/property/combinational_processes.pp |  2 ++
 data/property/impossible_processes.pp    |  2 ++
 data/property/incrementer.pp             |  3 +++
 data/property/incrementer.pro            | 15 ++++++------
 data/property/likely_a_clock.pp          |  3 +++
 data/property/simple_flip_flop.pp        |  4 ++++
 data/property/simple_flip_flop.pro       | 41 ++++++++++++++++++++++++++++++++
 data/property/unread_waveforms.pro       | 10 --------
 instr-to-kodkod/Makefile                 |  5 ++--
 sol-pretty-printer/Makefile              |  4 ++--
 sol-pretty-printer/src/Solutions.java    |  3 ++-
 11 files changed, 69 insertions(+), 23 deletions(-)
 create mode 100644 data/property/combinational_processes.pp
 create mode 100644 data/property/impossible_processes.pp
 create mode 100644 data/property/incrementer.pp
 create mode 100644 data/property/likely_a_clock.pp
 create mode 100644 data/property/simple_flip_flop.pp
 create mode 100644 data/property/simple_flip_flop.pro
 delete mode 100644 data/property/unread_waveforms.pro

diff --git a/data/property/combinational_processes.pp b/data/property/combinational_processes.pp
new file mode 100644
index 0000000..7d73bf9
--- /dev/null
+++ b/data/property/combinational_processes.pp
@@ -0,0 +1,2 @@
+The processus $ps.LABEL$ (from file $ps.FILE$, line $ps.LINE$, column
+$ps.COLUMN$) is combinational.
diff --git a/data/property/impossible_processes.pp b/data/property/impossible_processes.pp
new file mode 100644
index 0000000..a13e0e5
--- /dev/null
+++ b/data/property/impossible_processes.pp
@@ -0,0 +1,2 @@
+The process $ps.LABEL$ (from file $ps.FILE$, line $ps.LINE$, column
+$ps.COLUMN$) does not write anything and is thus unlikely to have any effect.
diff --git a/data/property/incrementer.pp b/data/property/incrementer.pp
new file mode 100644
index 0000000..5fe3e96
--- /dev/null
+++ b/data/property/incrementer.pp
@@ -0,0 +1,3 @@
+The waveform associated with $wf.IDENTIFIER$ (from file $wf.FILE$, line $wf.LINE$
+column $wf.COLUMN$) is incremented by the process $ps.LABEL$ (from
+$ps.FILE$, line $ps.line$, column $ps.COLUMN$).
diff --git a/data/property/incrementer.pro b/data/property/incrementer.pro
index ba8fc7a..4bc06ae 100644
--- a/data/property/incrementer.pro
+++ b/data/property/incrementer.pro
@@ -1,15 +1,14 @@
 (tag_existing
    (
       (wf waveform INCREMENTED_WAVEFORM)
+      (ps process INCREMENTER_PROCESS)
    )
-   (exists ps process
-      (CTL_verifies ps
-         (EF
-            (and
-               (is_read_structure "(??L)")
-               (is_read_element "0" "+")
-               (is_read_element "1" wf)
-            )
+   (CTL_verifies ps
+      (EF
+         (and
+            (is_read_structure "(??L)")
+            (is_read_element "0" "+")
+            (is_read_element "1" wf)
          )
       )
    )
diff --git a/data/property/likely_a_clock.pp b/data/property/likely_a_clock.pp
new file mode 100644
index 0000000..aea7af2
--- /dev/null
+++ b/data/property/likely_a_clock.pp
@@ -0,0 +1,3 @@
+The port $clock.IDENTIFIER$ (from file $clock.FILE$, line $clock.LINE$, column
+$clock.COLUMN$) is passed as parameter of either a rising_edge or a falling_edge
+function, making it likely to be a clock.
diff --git a/data/property/simple_flip_flop.pp b/data/property/simple_flip_flop.pp
new file mode 100644
index 0000000..fbad237
--- /dev/null
+++ b/data/property/simple_flip_flop.pp
@@ -0,0 +1,4 @@
+The process $ps.LABEL$ (declared in $ps.FILE$, l. $ps.LINE$, c. $ps.COLUMN$)
+describes a simple flip-flop 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.pro b/data/property/simple_flip_flop.pro
new file mode 100644
index 0000000..ea67575
--- /dev/null
+++ b/data/property/simple_flip_flop.pro
@@ -0,0 +1,41 @@
+(tag_existing
+   (
+      (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)
+      (is_in_sensitivity_list clk ps)
+      (CTL_verifies ps
+         (AF
+            (and
+               (kind "if")
+               (is_read_structure "(??)")
+               (or
+                  (is_read_element "0" "falling_edge")
+                  (is_read_element "0" "rising_edge")
+               )
+               (is_read_element "1" clk)
+               (EX
+                  (and
+                     (has_option "COND_WAS_TRUE")
+                     (does_not_reach_parent_before
+                        (and
+                           (expr_writes reg)
+                           (AX
+                              (not
+                                 (EF
+                                    (expr_writes reg)
+                                 )
+                              )
+                           )
+                        )
+                     )
+                  )
+               )
+            )
+         )
+      )
+   )
+)
diff --git a/data/property/unread_waveforms.pro b/data/property/unread_waveforms.pro
deleted file mode 100644
index b53862b..0000000
--- a/data/property/unread_waveforms.pro
+++ /dev/null
@@ -1,10 +0,0 @@
-(tag_existing
-   (
-      (wf waveform UNREAD_WAVEFORM)
-   )
-   (not
-      (exists ps process
-         (is_accessed_by wf ps)
-      )
-   )
-)
diff --git a/instr-to-kodkod/Makefile b/instr-to-kodkod/Makefile
index 60ad8da..1fe4535 100644
--- a/instr-to-kodkod/Makefile
+++ b/instr-to-kodkod/Makefile
@@ -100,7 +100,7 @@ PARSER_CLASSES = $(PARSER_SOURCES:.g4=.class)
 
 export
 ## Makefile Rules ##############################################################
-run: cfg-generator $(PARSER_CLASSES) $(SOLUTION_FILES) $(CLASSES)
+run: cfg-generator $(PARSER_CLASSES) $(CLASSES) $(SOLUTION_FILES)
 
 cfg-generator:
 	$(MAKE) -C cfg-to-paths
@@ -114,7 +114,8 @@ clean:
 	rm -f $(CLASSES)
 	rm -f $(SOL_DIR)/*.sol
 
-%.sol: cfg-generator $(PARSER_CLASSES) $(CLASSES) $(PROPERTY_FILES) $(MODEL_FILES) $(LEVEL_FILES)
+$(SOL_DIR)/%.sol: $(PROPERTY_FILES) $(MODEL_FILES) $(LEVEL_FILES)
+	touch $@
 	$(JAVA) -cp $(CLASSPATH) Main $@ \
 		$(filter %$(basename $(notdir $@)).pro,$(PROPERTY_FILES)) \
 		$(LEVEL_FILES) \
diff --git a/sol-pretty-printer/Makefile b/sol-pretty-printer/Makefile
index 4c5d954..b983157 100644
--- a/sol-pretty-printer/Makefile
+++ b/sol-pretty-printer/Makefile
@@ -56,10 +56,10 @@ CLASSES = $(SOURCES:.java=.class)
 SOLUTION_FILES = $(wildcard $(SOL_DIR)/*.sol)
 PROPERTY_PP_FILES = $(PROPERTY_FILES:.pro=.pp)
 SOLUTION_PP_PAIRS = \
-	$(foreach sf,$(SOLUTION_FILES),"$(sf) $(filter %$(basename $(notdir $(sf))).pp,$(PROPERTY_PP_FILES))")
+	$(foreach sf,$(SOLUTION_FILES),$(sf) $(filter %$(basename $(notdir $(sf))).pp,$(PROPERTY_PP_FILES)))
 
 run: $(SOLUTION_PP_PAIRS) $(MODEL_DIR)/structural.mod $(MODEL_DIR)/string_to_instr.map $(CLASSES)
-	$(JAVA) $(MODEL_DIR)/structural.mod $(MODEL_DIR)/string_to_instr.map $(SOLUTION_PP_PAIRS)
+	$(JAVA) -cp $(CLASSPATH) Main $(MODEL_DIR)/structural.mod $(MODEL_DIR)/string_to_instr.map $(SOLUTION_PP_PAIRS)
 
 %.class: %.java
 	$(JAVAC) -cp $(CLASSPATH) $<
diff --git a/sol-pretty-printer/src/Solutions.java b/sol-pretty-printer/src/Solutions.java
index 38a426a..0129794 100644
--- a/sol-pretty-printer/src/Solutions.java
+++ b/sol-pretty-printer/src/Solutions.java
@@ -84,7 +84,8 @@ public class Solutions
                      + me.getKey().toUpperCase()
                      + "$"
                   ),
-                  Strings.get_string_from_id(me.getValue())
+                  /* FIXME */
+                  (Strings.get_string_from_id(me.getValue()) == null) ? "null" : Strings.get_string_from_id(me.getValue())
                );
          }
       }
-- 
cgit v1.2.3-70-g09d2