| summaryrefslogtreecommitdiff |
diff options
Diffstat (limited to 'data')
| -rw-r--r-- | data/instructions/example_process.pl.kk | 88 | ||||
| -rw-r--r-- | data/level/control_flow_level.lvl (renamed from data/level/control_flow_level.data) | 5 | ||||
| -rw-r--r-- | data/level/control_flow_level_kodkod.lvl (renamed from data/level/control_flow_level_kodkod.data) | 3 | ||||
| -rw-r--r-- | data/level/structural_level.lvl (renamed from data/level/structural_level.data) | 0 | ||||
| -rw-r--r-- | data/property/unread_waveforms.pro | 10 |
5 files changed, 106 insertions, 0 deletions
diff --git a/data/instructions/example_process.pl.kk b/data/instructions/example_process.pl.kk new file mode 100644 index 0000000..c4f07b3 --- /dev/null +++ b/data/instructions/example_process.pl.kk @@ -0,0 +1,88 @@ +(add_element path p237_0) +(is_path_of p237_0 237) +(contains_node p237_0 262) +(is_before p237_0 262 263) +(contains_node p237_0 263) +(add_element path p237_1) +(is_path_of p237_1 262) +(contains_node p237_1 263) +(add_element path p237_2) +(is_path_of p237_2 237) +(contains_node p237_2 260) +(is_before p237_2 260 261) +(contains_node p237_2 261) +(add_element path p237_3) +(is_path_of p237_3 260) +(contains_node p237_3 261) +(add_element path p237_4) +(is_path_of p237_4 237) +(contains_node p237_4 258) +(is_before p237_4 258 259) +(contains_node p237_4 259) +(add_element path p237_5) +(is_path_of p237_5 258) +(contains_node p237_5 259) +(add_element path p237_6) +(is_path_of p237_6 237) +(contains_node p237_6 256) +(is_before p237_6 256 257) +(contains_node p237_6 257) +(add_element path p237_7) +(is_path_of p237_7 256) +(contains_node p237_7 257) +(add_element path p237_8) +(is_path_of p237_8 237) +(contains_node p237_8 254) +(is_before p237_8 254 255) +(contains_node p237_8 255) +(add_element path p237_9) +(is_path_of p237_9 254) +(contains_node p237_9 255) +(add_element path p237_10) +(is_path_of p237_10 237) +(contains_node p237_10 252) +(is_before p237_10 252 253) +(contains_node p237_10 253) +(add_element path p237_11) +(is_path_of p237_11 252) +(contains_node p237_11 253) +(add_element path p237_12) +(is_path_of p237_12 237) +(contains_node p237_12 250) +(is_before p237_12 250 251) +(contains_node p237_12 251) +(add_element path p237_13) +(is_path_of p237_13 250) +(contains_node p237_13 251) +(add_element path p237_14) +(is_path_of p237_14 237) +(contains_node p237_14 248) +(is_before p237_14 248 249) +(contains_node p237_14 249) +(add_element path p237_15) +(is_path_of p237_15 248) +(contains_node p237_15 249) +(add_element path p237_16) +(is_path_of p237_16 237) +(contains_node p237_16 246) +(is_before p237_16 246 247) +(contains_node p237_16 247) +(add_element path p237_17) +(is_path_of p237_17 246) +(contains_node p237_17 247) +(add_element path p237_18) +(is_path_of p237_18 237) +(contains_node p237_18 244) +(is_before p237_18 244 245) +(contains_node p237_18 245) +(add_element path p237_19) +(is_path_of p237_19 244) +(contains_node p237_19 245) +(add_element path p237_20) +(is_path_of p237_20 237) +(contains_node p237_20 239) +(is_before p237_20 239 242) +(contains_node p237_20 242) +(add_element path p237_21) +(is_path_of p237_21 239) +(contains_node p237_21 242) diff --git a/data/level/control_flow_level.data b/data/level/control_flow_level.lvl index a7cc9c0..516f9ef 100644 --- a/data/level/control_flow_level.data +++ b/data/level/control_flow_level.lvl @@ -7,6 +7,11 @@ (add_type node) (add_type node_depth) +;; Redundancies +(add_type process) +(add_type string) +(add_type waveform) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; PREDICATES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; diff --git a/data/level/control_flow_level_kodkod.data b/data/level/control_flow_level_kodkod.lvl index ed11735..949f69f 100644 --- a/data/level/control_flow_level_kodkod.data +++ b/data/level/control_flow_level_kodkod.lvl @@ -6,6 +6,9 @@ (add_type path) +;; Redundancies +(add_type node) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; PREDICATES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; diff --git a/data/level/structural_level.data b/data/level/structural_level.lvl index 75c4ac9..75c4ac9 100644 --- a/data/level/structural_level.data +++ b/data/level/structural_level.lvl diff --git a/data/property/unread_waveforms.pro b/data/property/unread_waveforms.pro new file mode 100644 index 0000000..b53862b --- /dev/null +++ b/data/property/unread_waveforms.pro @@ -0,0 +1,10 @@ +(tag_existing + ( + (wf waveform UNREAD_WAVEFORM) + ) + (not + (exists ps process + (is_accessed_by wf ps) + ) + ) +) |