summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/hastabel/Variables.java6
-rw-r--r--src/hastabel/lang/CTLVerifies.java15
-rw-r--r--src/hastabel/lang/Equals.java10
-rw-r--r--src/hastabel/lang/FunctionCall.java10
-rw-r--r--src/hastabel/lang/OperatorFormula.java10
-rw-r--r--src/hastabel/lang/PredicateFormula.java15
-rw-r--r--src/hastabel/lang/Quantifier.java15
7 files changed, 81 insertions, 0 deletions
diff --git a/src/hastabel/Variables.java b/src/hastabel/Variables.java
index 0ec7aac..de22b46 100644
--- a/src/hastabel/Variables.java
+++ b/src/hastabel/Variables.java
@@ -4,6 +4,7 @@ import hastabel.lang.Type;
import hastabel.lang.Variable;
import hastabel.lang.Expression;
+import java.util.Collection;
import java.util.HashMap;
import java.util.Map;
@@ -40,6 +41,11 @@ public class Variables
return var;
}
+ public Collection<Variable> get_all_seeked ()
+ {
+ return seeked.values();
+ }
+
public Variable add_variable (final Type type, final String var_name)
{
final Variable result;
diff --git a/src/hastabel/lang/CTLVerifies.java b/src/hastabel/lang/CTLVerifies.java
index 87abcd8..595e473 100644
--- a/src/hastabel/lang/CTLVerifies.java
+++ b/src/hastabel/lang/CTLVerifies.java
@@ -19,4 +19,19 @@ public class CTLVerifies extends Formula
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;
+ }
}
diff --git a/src/hastabel/lang/Equals.java b/src/hastabel/lang/Equals.java
index eba7a0c..639f2ea 100644
--- a/src/hastabel/lang/Equals.java
+++ b/src/hastabel/lang/Equals.java
@@ -11,4 +11,14 @@ public class Equals extends Formula
this.a = a;
this.b = b;
}
+
+ public Expression get_first_operand ()
+ {
+ return a;
+ }
+
+ public Expression get_second_operand ()
+ {
+ return b;
+ }
}
diff --git a/src/hastabel/lang/FunctionCall.java b/src/hastabel/lang/FunctionCall.java
index c71738e..6ec254e 100644
--- a/src/hastabel/lang/FunctionCall.java
+++ b/src/hastabel/lang/FunctionCall.java
@@ -17,4 +17,14 @@ class FunctionCall extends Expression
this.parent = parent;
this.params = params;
}
+
+ public Predicate get_function ()
+ {
+ return parent;
+ }
+
+ public List<Expression> get_arguments ()
+ {
+ return params;
+ }
}
diff --git a/src/hastabel/lang/OperatorFormula.java b/src/hastabel/lang/OperatorFormula.java
index 39b6bea..617299c 100644
--- a/src/hastabel/lang/OperatorFormula.java
+++ b/src/hastabel/lang/OperatorFormula.java
@@ -16,4 +16,14 @@ class OperatorFormula extends Formula
this.parent = parent;
this.params = params;
}
+
+ public Operator get_operator ()
+ {
+ return parent;
+ }
+
+ public List<Formula> get_operands ()
+ {
+ return params;
+ }
}
diff --git a/src/hastabel/lang/PredicateFormula.java b/src/hastabel/lang/PredicateFormula.java
index 566c1bd..029af6a 100644
--- a/src/hastabel/lang/PredicateFormula.java
+++ b/src/hastabel/lang/PredicateFormula.java
@@ -19,4 +19,19 @@ class PredicateFormula extends Formula
this.signature = signature;
this.params = params;
}
+
+ public Predicate get_predicate ()
+ {
+ return parent;
+ }
+
+ public List<Expression> get_parameters ()
+ {
+ return params;
+ }
+
+ public List<Type> get_signature ()
+ {
+ return signature;
+ }
}
diff --git a/src/hastabel/lang/Quantifier.java b/src/hastabel/lang/Quantifier.java
index aa05ebe..fbb6d75 100644
--- a/src/hastabel/lang/Quantifier.java
+++ b/src/hastabel/lang/Quantifier.java
@@ -19,4 +19,19 @@ public class Quantifier extends Formula
this.formula = formula;
this.is_forall = is_forall;
}
+
+ public boolean is_forall ()
+ {
+ return is_forall;
+ }
+
+ public Variable get_variable ()
+ {
+ return parent;
+ }
+
+ public Formula get_formula ()
+ {
+ return formula;
+ }
}