CTLVerifies is directly converted to first-order.

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;
-   }
-}