From d48380bd87dcef4b095b2a4e578d4461e68df73c Mon Sep 17 00:00:00 2001 From: Nathanael Sensfelder Date: Mon, 17 Jul 2017 15:22:19 +0200 Subject: Working on a way to CTL over DAG in Kodkod. --- data/level/control_flow_level.data | 18 ++++++++++++++++++ data/level/control_flow_level_kodkod.data | 13 +++++++++++++ 2 files changed, 31 insertions(+) create mode 100644 data/level/control_flow_level.data create mode 100644 data/level/control_flow_level_kodkod.data (limited to 'data') diff --git a/data/level/control_flow_level.data b/data/level/control_flow_level.data new file mode 100644 index 0000000..a880606 --- /dev/null +++ b/data/level/control_flow_level.data @@ -0,0 +1,18 @@ +;; Control Flow Level + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; TYPES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(add_type node) +(add_type node_depth) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; PREDICATES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(add_predicate has_kind node string) +(add_predicate has_option node string) +(add_predicate has_depth node node_depth) +(add_predicate node_connect node node) +(add_predicate expr_writes node waveform) +(add_predicate expr_reads node waveform) diff --git a/data/level/control_flow_level_kodkod.data b/data/level/control_flow_level_kodkod.data new file mode 100644 index 0000000..987b63e --- /dev/null +++ b/data/level/control_flow_level_kodkod.data @@ -0,0 +1,13 @@ +;; Control Flow Level, Kodkod additions + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; TYPES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(add_type path) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; PREDICATES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(add_predicate is_path_of path node) +(add_predicate contains_node path node) -- cgit v1.2.3-70-g09d2