summaryrefslogtreecommitdiff |
diff options
-rw-r--r-- | src/hastabel/PropertyParser.g4 | 21 | ||||
-rw-r--r-- | src/hastabel/lang/CTLVerifies.java | 37 |
2 files changed, 20 insertions, 38 deletions
diff --git a/src/hastabel/PropertyParser.g4 b/src/hastabel/PropertyParser.g4 index 0042c56..c58f0a6 100644 --- a/src/hastabel/PropertyParser.g4 +++ b/src/hastabel/PropertyParser.g4 @@ -593,6 +593,7 @@ ctl_verifies_operator [Variable current_node] (WS)* R_PAREN { + final hastabel.lang.Predicate is_start_node; final Variable process; if (current_node != null) @@ -612,9 +613,27 @@ ctl_verifies_operator [Variable current_node] WORLD.invalidate(); } + is_start_node = WORLD.get_predicates_manager().get("is_start_node"); + + if (is_start_node == null) + { + WORLD.invalidate(); + } + + is_start_node.mark_as_used(); + process = WORLD.get_variables_manager().get(($ps.text)); - $result = new CTLVerifies(root_node, process, ($f.result)); + $result = + Formula.exists + ( + root_node, + Formula.and + ( + is_start_node.as_formula_(root_node, process), + ($f.result) + ) + ); } ; diff --git a/src/hastabel/lang/CTLVerifies.java b/src/hastabel/lang/CTLVerifies.java deleted file mode 100644 index 595e473..0000000 --- a/src/hastabel/lang/CTLVerifies.java +++ /dev/null @@ -1,37 +0,0 @@ -package hastabel.lang; - -import java.util.List; - -public class CTLVerifies extends Formula -{ - private final Variable root_node; - private final Expression parent; - private final Formula formula; - - public CTLVerifies - ( - final Variable root_node, - final Expression parent, - final Formula formula - ) - { - this.root_node = root_node; - this.parent = parent; - this.formula = formula; - } - - public Variable get_root_node () - { - return root_node; - } - - public Expression get_process_expression () - { - return parent; - } - - public Formula get_ctl_formula () - { - return formula; - } -} |