aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNathanael Sensfelder <SpamShield0@MultiAgentSystems.org>2017-08-04 12:47:30 +0200
committerNathanael Sensfelder <SpamShield0@MultiAgentSystems.org>2017-08-04 12:47:30 +0200
commitd18ca72caf2004c7725b3de670c7397c5bf85eb4 (patch)
treece0d95cd60f2e9bac26015e645e4f33c165b8713
parentc4914a0649090b4784b72909eab53ea01e20a93e (diff)
downloadtabellion-improved_makefiles.zip
tabellion-improved_makefiles.tar.bz2
For some reason, CNE_01700 no longer works.improved_makefiles
-rw-r--r--data/property/combinational_processes.pp2
-rw-r--r--data/property/impossible_processes.pp2
-rw-r--r--data/property/incrementer.pp3
-rw-r--r--data/property/incrementer.pro15
-rw-r--r--data/property/likely_a_clock.pp3
-rw-r--r--data/property/simple_flip_flop.pp4
-rw-r--r--data/property/simple_flip_flop.pro41
-rw-r--r--data/property/unread_waveforms.pro10
-rw-r--r--instr-to-kodkod/Makefile5
-rw-r--r--sol-pretty-printer/Makefile4
-rw-r--r--sol-pretty-printer/src/Solutions.java3
11 files changed, 69 insertions, 23 deletions
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())
);
}
}