summaryrefslogtreecommitdiff |
diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/hastabel/Variables.java | 6 | ||||
-rw-r--r-- | src/hastabel/lang/CTLVerifies.java | 15 | ||||
-rw-r--r-- | src/hastabel/lang/Equals.java | 10 | ||||
-rw-r--r-- | src/hastabel/lang/FunctionCall.java | 10 | ||||
-rw-r--r-- | src/hastabel/lang/OperatorFormula.java | 10 | ||||
-rw-r--r-- | src/hastabel/lang/PredicateFormula.java | 15 | ||||
-rw-r--r-- | src/hastabel/lang/Quantifier.java | 15 |
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; + } } |