From 35bce44858fcd7b0dab398cbce72d13057d3a501 Mon Sep 17 00:00:00 2001
From: Nathanael Sensfelder <SpamShield0@MultiAgentSystems.org>
Date: Wed, 19 Jul 2017 15:31:05 +0200
Subject: forgot to use cfg-to-path. Still broken though.

---
 cfg-to-paths/Makefile                  | 18 ++++++++++--------
 data/property/impossible_processes.pro | 12 ++++++++++++
 instr-to-kodkod/Makefile               |  4 ++--
 instr-to-kodkod/src/Main.java          |  9 ++++++++-
 4 files changed, 32 insertions(+), 11 deletions(-)
 create mode 100644 data/property/impossible_processes.pro

diff --git a/cfg-to-paths/Makefile b/cfg-to-paths/Makefile
index c4d71e2..f0207ae 100644
--- a/cfg-to-paths/Makefile
+++ b/cfg-to-paths/Makefile
@@ -1,8 +1,6 @@
 ## Target(s) Configuration #####################################################
-MODEL_FILE = "../data/instructions/example_process.pl"
-ROOT_NODE = "237"
-ID_PREFIX = "p237_"
-OUTPUT_FILE = "$(MODEL_FILE).kk"
+MODEL_FILES = $(wildcard ../instr-scripts/pfp_*.mod)
+OUTPUT_FILES = $(patsubst ../instr-scripts/%.mod,%.cfg.mod,$(MODEL_FILES))
 
 ## Executables #################################################################
 JAVAC = javac
@@ -17,14 +15,18 @@ CLASSES = $(SOURCES:.java=.class)
 
 ## Makefile Rules ##############################################################
 
-all: $(CLASSES)
+all: $(CLASSES) $(OUTPUT_FILES)
 
 clean:
 	rm -f $(CLASSES)
 
-run: $(CLASSES)
-	$(JAVA) -cp $(CLASSPATH) Main $(MODEL_FILE) $(ROOT_NODE) $(ID_PREFIX) \
-		$(OUTPUT_FILE)
+#run: $(CLASSES)
+#	$(JAVA) -cp $(CLASSPATH) Main $(MODEL_FILE) $(ROOT_NODE) $(ID_PREFIX) \
+#		$(OUTPUT_FILE)
 
 %.class: %.java
 	$(JAVAC) -cp $(CLASSPATH) $<
+
+%.cfg.mod: ../instr-scripts/%.mod $(CLASSES)
+	$(eval ROOT_NODE := $(shell head -n 1 $< | grep "[0-9]\+" -o))
+	$(JAVA) -cp $(CLASSPATH) Main $< $(ROOT_NODE) "p$(ROOT_NODE)_" $@
diff --git a/data/property/impossible_processes.pro b/data/property/impossible_processes.pro
new file mode 100644
index 0000000..a93e916
--- /dev/null
+++ b/data/property/impossible_processes.pro
@@ -0,0 +1,12 @@
+(tag_existing
+   (
+      (ps process WHAT_ARE_YOU_DOING)
+   )
+   (forall sl1 waveform
+      (CTL_verifies ps
+         (not
+            (EF (expr_writes sl1))
+         )
+      )
+   )
+)
diff --git a/instr-to-kodkod/Makefile b/instr-to-kodkod/Makefile
index 3e69ba5..fe40d91 100644
--- a/instr-to-kodkod/Makefile
+++ b/instr-to-kodkod/Makefile
@@ -1,9 +1,9 @@
 ## Target(s) Configuration #####################################################
 #MODEL_FILES = $(wildcard ../data/instructions/*.mod)
-MODEL_FILES = ../instr-scripts/structural.mod $(wildcard ../instr-scripts/pfp_*.mod)
+MODEL_FILES = ../instr-scripts/structural.mod $(wildcard ../instr-scripts/pfp_*.mod) $(wildcard ../cfg-to-paths/pfp_*.mod)
 LEVEL_DIR = $(wildcard ../data/level/*.lvl)
 #PROPERTY_FILE = ../data/property/unread_waveforms.pro
-PROPERTY_FILE = ../data/property/combinational_processes.pro
+PROPERTY_FILE = ../data/property/impossible_processes.pro
 VAR_PREFIX = "_anon_"
 
 ## Executables #################################################################
diff --git a/instr-to-kodkod/src/Main.java b/instr-to-kodkod/src/Main.java
index e6b5750..5b0e9b5 100644
--- a/instr-to-kodkod/src/Main.java
+++ b/instr-to-kodkod/src/Main.java
@@ -188,7 +188,14 @@ public class Main
 
       while (solutions.hasNext())
       {
-         System.out.println(solutions.next());
+         final Solution sol;
+
+         sol = solutions.next();
+
+         if (sol.sat())
+         {
+            System.out.println(sol);
+         }
       }
    }
 }
-- 
cgit v1.2.3-70-g09d2