Got some property dependencies to work.

16 files changed, 221 insertions, 96 deletions

diff --git a/Makefile b/Makefile
index e60aa8d..1f72ef0 100644
--- a/Makefile
+++ b/Makefile
@@ -1,10 +1,10 @@
 ## Makefile Parameters #########################################################
-LEVEL_FILES ?= $(wildcard ${CURDIR}/data/level/*.lvl)
-ALL_PROPERTY_FILES ?= $(wildcard ${CURDIR}/data/property/*.pro)
-#PROPERTY_FILES ?= $(wildcard ${CURDIR}/data/property/*.pro)
-PROPERTY_FILES ?= $(wildcard ${CURDIR}/data/property/test.pro)
+LEVELS_DIR ?= ${CURDIR}/data/level/
+PROPERTIES_DIR ?= ${CURDIR}/data/property/
+PROPERTIES ?= $(basename $(notdir $(wildcard $(PROPERTIES_DIR)/*.pro)))
 AST_FILE ?= ${CURDIR}/data/ast/best_chronometer_ever.xml
 TEMPLATE_DIR ?= ${CURDIR}/data/template/
+TO_PRED_TEMPLATE_DIR ?= ${CURDIR}/data/to_pred_template/
 #AST_FILE = ${CURDIR}/data/ast/pong.xml
 NICE_MESSAGE ?=
 
@@ -14,22 +14,27 @@ MODEL_DIR ?= $(TMP_DIR)/mod
 MODEL_INSTANCES_DIR ?= $(MODEL_DIR)/instance
 MODEL_INFERRED_DIR ?= $(MODEL_DIR)/inferred
 SOL_DIR ?= $(TMP_DIR)/sol
+INFERRED_LEVEL_FILE ?= $(LEVELS_DIR)/inferred.lvl
 
 ## Sub-programs ################################################################
 AST_TO_INSTR ?= ast-to-instr
 INST_CALC ?= instance-calculator
 SOLVER ?= instr-to-kodkod
 PRETTY_PRINTER ?= sol-pretty-printer
+PROP_TO_PRED ?= prop_to_pred
 
 export
 
 ################################################################################
+ALL_PROPERTY_FILES = $(wildcard $(PROPERTIES_DIR)/*.pro)
+
 ALL_DIRS = \
 	$(TMP_DIR) \
 	$(DEPENDENCIES_DIR) \
 	$(MODEL_DIR) \
 	$(MODEL_INSTANCES_DIR) \
-	$(MODEL_INFERED_DIR) \
+	$(TO_PRED_TEMPLATE_DIR) \
+	$(MODEL_INFERRED_DIR) \
 	$(SOL_DIR)
 
 all: $(ALL_DIRS)
@@ -42,36 +47,43 @@ compile:
 	$(MAKE) -C $(INST_CALC) compile
 	$(MAKE) -C $(SOLVER) compile
 	$(MAKE) -C $(PRETTY_PRINTER) compile
+	$(MAKE) -C $(PROP_TO_PRED) compile
 
 model:
 	$(MAKE) -C $(AST_TO_INSTR) model
 	$(MAKE) -C $(INST_CALC) model
 	$(MAKE) -C $(SOLVER) model
 	$(MAKE) -C $(PRETTY_PRINTER) model
+	$(MAKE) -C $(PROP_TO_PRED) 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
+	$(MAKE) -C $(PROP_TO_PRED) solutions
 
 clean:
 	$(MAKE) -C $(AST_TO_INSTR) clean
 	$(MAKE) -C $(INST_CALC) clean
 	$(MAKE) -C $(SOLVER) clean
 	$(MAKE) -C $(PRETTY_PRINTER) clean
+	$(MAKE) -C $(PROP_TO_PRED) 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
+	$(MAKE) -C $(PROP_TO_PRED) 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
+	$(MAKE) -C $(PROP_TO_PRED) clean_solutions
 
 $(ALL_DIRS):
 	mkdir -p $@
+
diff --git a/ast-to-instr/Makefile b/ast-to-instr/Makefile
index c8e9174..d5fc2d2 100644
--- a/ast-to-instr/Makefile
+++ b/ast-to-instr/Makefile
@@ -1,24 +1,16 @@
 ## Parameters ##################################################################
 #### GHDL's xml AST output.
-ifndef AST_FILE
-AST_FILE =
-endif
+AST_FILE ?=
 
 #### Where to output the models.
-ifndef MODEL_DIR
-MODEL_DIR =
-endif
+MODEL_DIR ?=
 
 #### Binaries
 ###### JRE binary
-ifndef JAVA
-JAVA = java
-endif
+JAVA ?= java
 
 ###### JDK binary
-ifndef JAVAC
-JAVAC = javac
-endif
+JAVAC ?= javac
 
 ## Parameters Sanity Check #####################################################
 ifeq ($(strip $(AST_FILE)),)
diff --git a/data/property/test.pro b/data/property/test.pro
new file mode 100644
index 0000000..9d2115c
--- /dev/null
+++ b/data/property/test.pro
@@ -0,0 +1,9 @@
+#require "simple_flip_flop"
+#require "combinational_processes"
+
+(tag_existing
+   (
+      (ps process SUSPICIOUS_PROCESS)
+   )
+   (_combinational_processes ps)
+)
diff --git a/data/template/fast.pp b/data/template/fast.pp
deleted file mode 100644
index b460eec..0000000
--- a/data/template/fast.pp
+++ /dev/null
@@ -1,6 +0,0 @@
-The component described by the entity $ent.IDENTIFIER$ (declared in $ent.FILE$,
-line $ent.LINE$, column $ent.COLUMN$) has a simple flip-flop described by the
-process $ps.LABEL$ (declared in $ps.FILE$, l. $ps.LINE$, c. $ps.COLUMN$),
-controlled by $clk.IDENTIFIER$ (declared in $clk.FILE$, l. $clk.LINE$,
-c. $clk.COLUMN$), and with output $reg.IDENTIFIER$ (declared in $reg.FILE$,
-l. $reg.LINE$, c. $reg.COLUMN$).
diff --git a/data/template/slow.pp b/data/template/slow.pp
deleted file mode 100644
index b460eec..0000000
--- a/data/template/slow.pp
+++ /dev/null
@@ -1,6 +0,0 @@
-The component described by the entity $ent.IDENTIFIER$ (declared in $ent.FILE$,
-line $ent.LINE$, column $ent.COLUMN$) has a simple flip-flop described by the
-process $ps.LABEL$ (declared in $ps.FILE$, l. $ps.LINE$, c. $ps.COLUMN$),
-controlled by $clk.IDENTIFIER$ (declared in $clk.FILE$, l. $clk.LINE$,
-c. $clk.COLUMN$), and with output $reg.IDENTIFIER$ (declared in $reg.FILE$,
-l. $reg.LINE$, c. $reg.COLUMN$).
diff --git a/data/template/test.pp b/data/template/test.pp
new file mode 100644
index 0000000..4ce45d7
--- /dev/null
+++ b/data/template/test.pp
@@ -0,0 +1 @@
+$ps.LABEL$ is suspicious.
diff --git a/instance-calculator/Makefile b/instance-calculator/Makefile
index 9dddc88..9002ca1 100644
--- a/instance-calculator/Makefile
+++ b/instance-calculator/Makefile
@@ -1,24 +1,16 @@
 ## Parameters ##################################################################
 #### Where to find the model
-ifndef MODEL_DIR
-MODEL_DIR =
-endif
+MODEL_DIR ?=
 
 #### Where to store the Instance model
-ifndef MODEL_INSTANCES_DIR
-MODEL_INSTANCES_DIR =
-endif
+MODEL_INSTANCES_DIR ?=
 
 #### Binaries
 ###### JRE binary
-ifndef JAVA
-JAVA = java
-endif
+JAVA ?= java
 
 ###### JDK binary
-ifndef JAVAC
-JAVAC = javac
-endif
+JAVAC ?= javac
 
 ## Parameters Sanity Check #####################################################
 ifeq ($(strip $(MODEL_DIR)),)
diff --git a/instance-calculator/src/QuickParser.java b/instance-calculator/src/QuickParser.java
index 383373e..ed74526 100644
--- a/instance-calculator/src/QuickParser.java
+++ b/instance-calculator/src/QuickParser.java
@@ -14,7 +14,7 @@ public class QuickParser
 
    static
    {
-      instr_pattern = Pattern.compile("\\((?<list>[a-z_0-9 \"]+)\\)");
+      instr_pattern = Pattern.compile("\\((?<list>[a-z_A-Z0-9 \"]+)\\)");
    }
    public QuickParser (final String filename)
    throws FileNotFoundException
diff --git a/instr-to-kodkod/Makefile b/instr-to-kodkod/Makefile
index 322205f..0523a46 100644
--- a/instr-to-kodkod/Makefile
+++ b/instr-to-kodkod/Makefile
@@ -1,57 +1,48 @@
 ## Parameters ##################################################################
 #### Where to find the level files
-ifndef LEVEL_FILES
-LEVEL_FILES =
-endif
+LEVEL_FILES ?= $(wildcard $(LEVELS_DIR)/*.lvl)
 
 #### Where to find the properties to verify
-ifndef PROPERTY_FILES
-PROPERTY_FILES =
-endif
+PROPERTIES_DIR ?=
 
-#### Where to find the model
-ifndef MODEL_DIR
-MODEL_DIR =
-endif
+#### What are the targetted properties
+PROPERTIES ?=
+
+#### Where to find the properties to verify
+ALL_PROPERTY_FILES ?= $(wildcard $(PROPERTIES_DIR)/*.pro)
+
+MODEL_DIR ?=
 
 #### Where to store & find the PATH models
-ifndef PATH_MODEL_DIR
-PATH_MODEL_DIR = $(MODEL_DIR)/path/
-endif
+PATH_MODEL_DIR ?= $(MODEL_DIR)/path/
 
 #### Where to output the solutions.
-ifndef SOL_DIR
-SOL_DIR =
-endif
+SOL_DIR ?=
 
 #### Where to get the missing Jar files.
-ifndef JAR_SOURCE
-JAR_SOURCE = "https://noot-noot.org/tabellion/jar/"
-endif
+JAR_SOURCE ?= "https://noot-noot.org/tabellion/jar/"
 
 #### Binaries
 ###### JRE binary
-ifndef JAVA
 JAVA = java
-endif
 
 ###### JDK binary
-ifndef JAVAC
 JAVAC = javac
-endif
 
 ##### Downloader
-ifndef DOWNLOADER
 DOWNLOADER = wget
-endif
 
 ## Parameters Sanity Check #####################################################
 ifeq ($(strip $(LEVEL_FILES)),)
 $(error No LEVEL_FILES defined as parameter.)
 endif
 
-ifeq ($(strip $(PROPERTY_FILES)),)
-$(error No PROPERTY_FILES defined as parameter.)
+ifeq ($(strip $(PROPERTIES_DIR)),)
+$(error No PROPERTIES_DIR defined as parameter.)
+endif
+
+ifeq ($(strip $(PROPERTIES)),)
+$(error No PROPERTIES defined as parameter.)
 endif
 
 ifeq ($(strip $(MODEL_DIR)),)
@@ -90,9 +81,9 @@ ANTLR_JAR = ${CURDIR}/antlr-4.7-complete.jar
 ## Makefile Magic ##############################################################
 SOURCES = $(wildcard src/*.java)
 CLASSES = $(SOURCES:.java=.class)
-SOLUTION_FILES = $(addprefix $(SOL_DIR)/,$(notdir $(PROPERTY_FILES:.pro=.sol)))
+SOLUTION_FILES = $(addsuffix .sol,$(addprefix $(SOL_DIR)/,$(notdir $(PROPERTIES))))
 DEPENDENCY_FILES = \
-	$(addprefix $(DEPENDENCIES_DIR)/,$(notdir $(PROPERTY_FILES:.pro=.deps)))
+	$(addprefix $(DEPENDENCIES_DIR)/,$(notdir $(ALL_PROPERTY_FILES:.pro=.deps)))
 MODEL_FILES = \
 	$(MODEL_DIR)/structural.mod \
 	$(MODEL_DIR)/depths.mod \
@@ -118,9 +109,11 @@ clean:
 	rm -f $(CLASSES)
 	rm -f $(SOL_DIR)/*.sol
 	rm -f $(DEPENDENCY_FILES)
+	rm -f $(wildcard $(MODEL_INFERRED_DIR)/*.mod)
 
 clean_model:
 	$(MAKE) -C cfg-to-paths clean_model
+	rm -f $(wildcard $(MODEL_INFERRED_DIR)/*.mod)
 
 clean_solutions:
 	rm -f $(SOL_DIR)/*.sol
@@ -133,18 +126,23 @@ cfg-generator:
 $(PARSER_CLASSES): antlr-4.7-complete.jar kodkod.jar $(PARSER_SOURCES)
 	$(MAKE) -C parser
 
-$(SOL_DIR)/%.sol: \
-	$(DEPENDENCIES_DIR)/%.deps $(PROPERTY_FILES) $(MODEL_FILES) $(LEVEL_FILES)
-	touch $@
+-include $(wildcard $(DEPENDENCIES_DIR)/*)
+
+$(SOLUTION_FILES): $(SOL_DIR)/%.sol: $(PROPERTIES_DIR)/%.pro \
+	$(SOL_DIR)/%.sol.ready $(MODEL_FILES) $(LEVEL_FILES)
+#	$(addprefix $(SOL_DIR)/,$(addsuffix .sol,$($(DEPENDENCIES_DIR)/%.deps)))
+	echo "$^"
 	$(JAVA) -cp $(CLASSPATH) Main $@ -v \
-		$(filter %$(basename $(notdir $@)).pro,$(PROPERTY_FILES)) \
+		$< \
 		$(LEVEL_FILES) \
 		$(MODEL_FILES) \
+		$(MODEL_INFERRED_DIR)/*.mod \
 		$(wildcard $(PATH_MODEL_DIR)/*.mod)
-
-$(DEPENDENCY_FILES): $(PROPERTY_FILES)
-	sed -n 's/^#require \"\(.*\)\"$$/\1/p' \
-		$(filter %$(basename $(notdir $@)).pro,$(PROPERTY_FILES)) > $@
+	echo "" >> $@
+	$(MAKE) -C .. \
+		PROPERTIES=$(basename $(notdir $@)) \
+		TEMPLATE_DIR=$(TO_PRED_TEMPLATE_DIR) \
+		NICE_MESSAGE=$(MODEL_INFERRED_DIR)/$(basename $(notdir $@)).mod
 
 src/%.class: src/%.java $(PARSER_CLASSES) $(REQUIRED_JARS)
 	$(JAVAC) -cp $(CLASSPATH) $<
@@ -152,3 +150,4 @@ src/%.class: src/%.java $(PARSER_CLASSES) $(REQUIRED_JARS)
 %.jar:
 	echo "Attempting to download missing jar '$@'..."
 	$(DOWNLOADER) "$(JAR_SOURCE)/$@"
+
diff --git a/instr-to-kodkod/cfg-to-paths/Makefile b/instr-to-kodkod/cfg-to-paths/Makefile
index 49c1e83..9dd0590 100644
--- a/instr-to-kodkod/cfg-to-paths/Makefile
+++ b/instr-to-kodkod/cfg-to-paths/Makefile
@@ -1,24 +1,16 @@
 ## Parameters ##################################################################
 #### Where to find the model
-ifndef MODEL_DIR
-MODEL_DIR =
-endif
+MODEL_DIR ?=
 
 #### Where to store the CFG models
-ifndef PATH_MODEL_DIR
-PATH_MODEL_DIR =
-endif
+PATH_MODEL_DIR ?=
 
 #### Binaries
 ###### JRE binary
-ifndef JAVA
-JAVA = java
-endif
+JAVA ?= java
 
 ###### JDK binary
-ifndef JAVAC
-JAVAC = javac
-endif
+JAVAC ?= javac
 
 ## Parameters Sanity Check #####################################################
 ifeq ($(strip $(MODEL_DIR)),)
diff --git a/instr-to-kodkod/cfg-to-paths/src/QuickParser.java b/instr-to-kodkod/cfg-to-paths/src/QuickParser.java
index 47cea27..eb1ba33 100644
--- a/instr-to-kodkod/cfg-to-paths/src/QuickParser.java
+++ b/instr-to-kodkod/cfg-to-paths/src/QuickParser.java
@@ -10,8 +10,9 @@ public class QuickParser
 
    static
    {
-      instr_pattern = Pattern.compile("\\((?<list>[a-z_0-9 \"]+)\\)");
+      instr_pattern = Pattern.compile("\\((?<list>[a-zA-Z_0-9 \"]+)\\)");
    }
+
    public QuickParser (final String filename)
    throws FileNotFoundException
    {
diff --git a/instr-to-kodkod/src/QuickParser.java b/instr-to-kodkod/src/QuickParser.java
index 6a75106..064deba 100644
--- a/instr-to-kodkod/src/QuickParser.java
+++ b/instr-to-kodkod/src/QuickParser.java
@@ -19,7 +19,7 @@ public class QuickParser
       instr_pattern =
          Pattern.compile
          (
-            "\\(([a-z_0-9\\->]+ .*)\\)"
+            "\\(([a-z_A-Z0-9\\->]+ .*)\\)"
          );
    }
 
diff --git a/prop_to_pred/Makefile b/prop_to_pred/Makefile
new file mode 100644
index 0000000..50cd36a
--- /dev/null
+++ b/prop_to_pred/Makefile
@@ -0,0 +1,53 @@
+## Parameters ##################################################################
+TO_PRED_TEMPLATE_DIR ?=
+INFERRED_LEVEL_FILE ?=
+PARSING_SCRIPT ?= ${CURDIR}/parser.py
+
+## Parameters Sanity Check #####################################################
+ifeq ($(strip $(PARSING_SCRIPT)),)
+$(error No PARSING_SCRIPT defined as parameter.)
+endif
+
+################################################################################
+
+## Makefile Magic ##############################################################
+PRED_TO_INFER = \
+	$(addprefix $(TO_PRED_TEMPLATE_DIR)/,$(notdir $(wildcard $(TEMPLATE_DIR)/*.pp)))
+ADDITIONAL_MAKEFILES = \
+	$(addsuffix .deps,$(addprefix $(DEPENDENCIES_DIR)/,$(basename $(notdir $(wildcard $(PROPERTIES_DIR)/*.pro)))))
+
+export
+## Makefile Rules ##############################################################
+compile: $(PRED_TO_INFER) $(ADDITIONAL_MAKEFILES)
+
+model:
+
+solutions:
+
+clean:
+	rm -f $(TO_PRED_TEMPLATE_DIR)/*
+	rm -f $(INFERRED_LEVEL_FILE)
+
+clean_model:
+
+clean_solutions:
+	rm -f $(TO_PRED_TEMPLATE_DIR)/*
+	rm -f $(INFERRED_LEVEL_FILE)
+
+########
+$(TO_PRED_TEMPLATE_DIR)/%.pp: $(PROPERTIES_DIR)/%.pro
+	cat $< | sed 's/.*;;.*//g' | tr -d "\n\r" \
+		| sed -n 's/.*(tag_existing[ \t]\+([ \t]*\(\([ \t]*([^)]\+)\)\+\)[ \t]*.*)/\1/p' \
+		| sed 's/)/)\n/g' | sed 's/[ \t]\+/ /g' | tr -d "()" \
+		| $(PARSING_SCRIPT) \
+			$(patsubst %.pp,%,$(notdir $(basename $@))) \
+			$@ \
+			$(INFERRED_LEVEL_FILE)
+	$(MAKE) $(DEPENDENCIES_DIR)/$(patsubst %.pp,%,$(notdir $(basename $@))).deps
+
+$(DEPENDENCIES_DIR)/%.deps: $(PROPERTIES_DIR)/%.pro
+	printf "$(SOL_DIR)/$(notdir $(basename $@)).sol.ready: " > $@
+	for dep in `sed -n 's/^#require \"\(.*\)\"$$/\1/p' $<` ; do \
+		printf "$(SOL_DIR)/$$dep.sol " >> $@ ; \
+	done
+	printf "\n\t touch $(SOL_DIR)/$(notdir $(basename $@)).sol.ready\n\n" >> $@
diff --git a/prop_to_pred/parser.py b/prop_to_pred/parser.py
new file mode 100755
index 0000000..7a25561
--- /dev/null
+++ b/prop_to_pred/parser.py
@@ -0,0 +1,78 @@
+#!/usr/bin/env python3
+import sys
+import argparse
+
+
+parser = argparse.ArgumentParser(
+    description='Property to Predicate parser.'
+)
+
+parser.add_argument(
+    "predicate_name",
+    action='store',
+    type=str,
+    help="Name of the predicate."
+)
+
+parser.add_argument(
+    "output_template_file",
+    action='store',
+    type=argparse.FileType(mode='w',encoding='UTF-8'),
+    help="Predicate from Property template file."
+)
+
+parser.add_argument(
+    "inferred_level",
+    action='store',
+    type=argparse.FileType(mode='a',encoding='UTF-8'),
+    help="Inferred level file."
+)
+
+args = parser.parse_args()
+
+var_names = list()
+var_types = list()
+
+for line in sys.stdin.readlines():
+    line_data = line.strip().split(" ")
+    print(line_data)
+    var_name = line_data[0].strip()
+    var_type = line_data[1].strip()
+
+    args.inferred_level.write("(add_type " + var_type + ")\n")
+
+    var_names.append(var_name)
+    var_types.append(var_type)
+
+args.inferred_level.write(
+    "(add_predicate _"
+    + args.predicate_name
+    + " "
+    + ' '.join(var_types)
+    + ")\n"
+)
+
+params = ""
+for i in range(len(var_types)):
+    if (var_types[i] == "waveform"):
+        new_id = ("$" + var_names[i] + ".WFM_ID$")
+    else:
+        new_id = ("$" + var_names[i] + ".ID$")
+
+    params += (" " + new_id)
+
+    args.output_template_file.write(
+        "(add_element "
+        + var_types[i]
+        + " "
+        + new_id
+        + ")\n"
+    )
+
+args.output_template_file.write(
+    "(_"
+    + args.predicate_name
+    + params
+    + ")\n"
+)
+
diff --git a/sol-pretty-printer/src/SolutionItem.java b/sol-pretty-printer/src/SolutionItem.java
index f251b62..7b23061 100644
--- a/sol-pretty-printer/src/SolutionItem.java
+++ b/sol-pretty-printer/src/SolutionItem.java
@@ -29,6 +29,7 @@ public class SolutionItem
       }
 
       FROM_ID.put(wfm_id, si);
+      si.function_values.put("wfm_id", wfm_id);
    }
 
    public static void handle_unary_set_function
diff --git a/sol-pretty-printer/src/Solutions.java b/sol-pretty-printer/src/Solutions.java
index 0129794..4b676b1 100644
--- a/sol-pretty-printer/src/Solutions.java
+++ b/sol-pretty-printer/src/Solutions.java
@@ -74,6 +74,10 @@ public class Solutions
 
          for (final Map.Entry<String, String> me: si.get_functions_data())
          {
+            final String keyword;
+
+            keyword = me.getKey().toUpperCase();
+
             pp_content =
                pp_content.replace
                (
@@ -81,11 +85,14 @@ public class Solutions
                      "$"
                      + sol_data[0]
                      + "."
-                     + me.getKey().toUpperCase()
+                     + keyword
                      + "$"
                   ),
-                  /* FIXME */
-                  (Strings.get_string_from_id(me.getValue()) == null) ? "null" : Strings.get_string_from_id(me.getValue())
+                  (
+                     keyword.endsWith("ID") ?
+                        me.getValue() :
+                        Strings.get_string_from_id(me.getValue())
+                  )
                );
          }
       }