summaryrefslogtreecommitdiff
path: root/instr-to-kodkod/parser
diff options
context:
space:
mode:
Diffstat (limited to 'instr-to-kodkod/parser')
-rw-r--r--instr-to-kodkod/parser/PropertyParser.g4329
1 files changed, 279 insertions, 50 deletions
diff --git a/instr-to-kodkod/parser/PropertyParser.g4 b/instr-to-kodkod/parser/PropertyParser.g4
index 516e927..2df87cb 100644
--- a/instr-to-kodkod/parser/PropertyParser.g4
+++ b/instr-to-kodkod/parser/PropertyParser.g4
@@ -20,48 +20,137 @@ options
/* of the class */
}
-prog: tag_existing;
+prog:
+ tag_existing
+;
-tag_existing
- : TAG_EXISTING_KW L_PAREN (tag_item)+ R_PAREN (WS)* sl_formula (WS)* R_PAREN
+tag_existing:
+ (WS)* TAG_EXISTING_KW
+ L_PAREN
+ (tag_item)+
+ R_PAREN
+ (WS)* sl_formula
+ (WS)* R_PAREN
;
-tag_item
- : (WS)* L_PAREN (WS)* ID (WS)+ ID (WS)+ ID (WS)* R_PAREN (WS)*
+tag_item:
+ (WS)* L_PAREN
+ (WS)* var=ID
+ (WS)+ type=ID
+ (WS)+ tag=ID
+ (WS)* R_PAREN
+ (WS)*
;
-predicate: (WS)* L_PAREN ID ((WS)+ ID)* (WS)* R_PAREN;
+id_list
+ returns [List<Variable> list]:
+
+ @init
+ {
+ final List<Variable> result = new ArrayList<Variable>();
+ }
+
+ (
+ (WS)+
+ var=ID
+ {
+ result.add(VARIABLE_SET.get_variable($var.text));
+ }
+ )*
+
+ {
+ $list = result;
+ }
+;
/******************************************************************************/
/** Structural Level **********************************************************/
/******************************************************************************/
+
+sl_predicate
+ return [Formula result]:
+
+ (WS)* L_PAREN
+ ID
+ id_list
+ (WS)* R_PAREN
+
+ {
+ /* TODO */
+ }
+;
+
+sl_non_empty_formula_list
+ returns [List<Formula> list]:
+
+ @init
+ {
+ final List<Formula> result = new ArrayList<Formula>();
+ }
+
+ (
+ sl_formula
+
+ {
+ result.add($sl_formula);
+ }
+ )+
+
+ {
+ $list = result;
+ }
+;
+
/**** First Order Expressions *************************************************/
-sl_and_operator returns [Formula result]:
- (WS)* AND_OPERATOR_KW a=sl_formula b=(sl_formula)+ (WS)* R_PAREN
+sl_and_operator
+ returns [Formula result]:
+
+ (WS)* AND_OPERATOR_KW
+ sl_formula
+ sl_non_empty_formula_list
+ (WS)* R_PAREN
+
{
/* TODO */
- $result = a.and(b);
+ $result = $sl_formula.and($sl_non_empty_formula_list);
}
;
-sl_or_operator returns [Formula result]:
- (WS)* OR_OPERATOR_KW a=sl_formula b=(sl_formula)+ (WS)* R_PAREN
+sl_or_operator
+ returns [Formula result]:
+
+ (WS)* OR_OPERATOR_KW
+ sl_formula
+ sl_non_empty_formula_list
+ (WS)* R_PAREN
+
{
/* TODO */
- $result = a.or(b);
+ $result = $sl_formula.or($sl_non_empty_formula_list);
}
;
-sl_not_operator returns [Formula result]:
- (WS)* NOT_OPERATOR_KW sl_formula (WS)* R_PAREN
+sl_not_operator
+ returns [Formula result]:
+
+ (WS)* NOT_OPERATOR_KW
+ sl_formula
+ (WS)* R_PAREN
+
{
/* TODO */
$result = $sl_formula.not();
}
;
-sl_implies_operator returns [Formula result]:
- (WS)* IMPLIES_OPERATOR_KW a=sl_formula b=sl_formula (WS)* R_PAREN
+sl_implies_operator
+ returns [Formula result]:
+
+ (WS)* IMPLIES_OPERATOR_KW
+ a=sl_formula
+ b=sl_formula
+ (WS)* R_PAREN
+
{
/* TODO */
$result = $a.implies($b);
@@ -69,8 +158,15 @@ sl_implies_operator returns [Formula result]:
;
/** Quantified Expressions ****************************************************/
-sl_exists_operator returns [Formula result]:
- (WS)* EXISTS_OPERATOR_KW var=ID (WS)+ type=ID f=sl_formula (WS*) R_PAREN
+sl_exists_operator
+ returns [Formula result]:
+
+ (WS)* EXISTS_OPERATOR_KW
+ var=ID
+ (WS)+ type=ID
+ f=sl_formula
+ (WS*) R_PAREN
+
{
/* TODO */
$result =
@@ -87,8 +183,15 @@ sl_exists_operator returns [Formula result]:
}
;
-sl_forall_operator returns [Formula result]:
- (WS)* FORALL_OPERATOR_KW var=ID (WS)+ type=ID f=sl_formula (WS*) R_PAREN
+sl_forall_operator
+ returns [Formula result]:
+
+ (WS)* FORALL_OPERATOR_KW
+ var=ID
+ (WS)+ type=ID
+ f=sl_formula
+ (WS*) R_PAREN
+
{
/* TODO */
$result =
@@ -96,7 +199,7 @@ sl_forall_operator returns [Formula result]:
(
VARIABLE_SET.get_variable
(
- $var
+ $var.text
).oneOf
(
MODEL.get_type_as_relation($type)
@@ -106,54 +209,80 @@ sl_forall_operator returns [Formula result]:
;
/** Special Expressions *******************************************************/
-sl_ctl_verifies_operator returns [Formula result]:
- (WS)* CTL_VERIFIES_OPERATOR_KW ps=ID (WS)* f=bl_formula (WS)* R_PAREN
+sl_ctl_verifies_operator
+ returns [Formula result]:
+
+ @init
+ {
+ final Variable root_node;
+
+ root_node = VARIABLE_SET.generate_new_state_variable();
+ }
+
+ (WS)* CTL_VERIFIES_OPERATOR_KW
+ ps=ID
+ f=bl_formula[root_node]
+ (WS)* R_PAREN
+
{
/* TODO */
+
$result =
$f.forSome
(
- VARIABLE_SET.get_variable
+ root_node.oneOf
(
- ???
- ).oneOf
- (
- {n | <ps, n> \in start_node}
+ MODEL.get_type_as_relation("node").in
+ (
+ VARIABLE_SET.get_variable($ps).join
+ (
+ MODEL.get_predicate_as_relation("start_node")
+ )
+ )
)
);
}
;
/**** Formula Definition ******************************************************/
-sl_formula returns [Formula result]:
- predicate
+sl_formula
+ returns [Formula result]:
+
+ sl_predicate
{
$result = $predicate;
}
+
| sl_and_operator
{
$result = $sl_and_operator;
}
+
| sl_or_operator
{
$result = $sl_or_operator;
}
+
| sl_not_operator
{
$result = $sl_not_operator;
}
+
| sl_implies_operator
{
$result = $sl_implies_operator;
}
+
| sl_exists_operator
{
$result = $sl_exists_operator;
}
+
| sl_forall_operator
{
$result = $sl_forall_operator;
}
+
| sl_ctl_verifies_operator
{
$result = $sl_ctl_verifies_operator;
@@ -163,33 +292,76 @@ sl_formula returns [Formula result]:
/******************************************************************************/
/** Behavioral Level **********************************************************/
/******************************************************************************/
+bl_formula_list [Variable current_state]
+ returns [List<Formula> list]:
+
+ @init
+ {
+ final List<Formula> result = new ArrayList<Formula>();
+ }
+
+ (
+ bl_formula[current_state]
+ {
+ result.add($bl_formula);
+ }
+ )+
+
+ {
+ $list = result;
+ }
+;
+
/**** First Order Expressions *************************************************/
-bl_and_operator returns [Formula result]:
- (WS)* AND_OPERATOR_KW a=bl_formula b=(bl_formula)+ (WS)* R_PAREN
+bl_and_operator [Variable current_state]
+ returns [Formula result]:
+
+ (WS)* AND_OPERATOR_KW
+ bl_formula[current_state]
+ bl_formula_list[current_state]
+ (WS)* R_PAREN
+
{
/* TODO */
- $result = $a.and($b);
+ $result = $bl_formula.and($bl_formula_list);
}
;
-bl_or_operator returns [Formula result]:
- (WS)* OR_OPERATOR_KW a=bl_formula b=(bl_formula)+ (WS)* R_PAREN
+bl_or_operator [Variable current_state]
+ returns [Formula result]:
+
+ (WS)* OR_OPERATOR_KW
+ bl_formula[current_state]
+ bl_formula_list[current_state]
+ (WS)* R_PAREN
+
{
/* TODO */
- $result = $a.or($b);
+ $result = $bl_formula.or($bl_formula_list);
}
;
-bl_not_operator returns [Formula result]:
- (WS)* NOT_OPERATOR_KW bl_formula (WS)* R_PAREN
+bl_not_operator [Variable current_state]
+ returns [Formula result]:
+
+ (WS)* NOT_OPERATOR_KW
+ bl_formula[current_state]
+ (WS)* R_PAREN
+
{
/* TODO */
$result = $bl_formula.not();
}
;
-bl_implies_operator returns [Formula result]:
- (WS)* IMPLIES_OPERATOR_KW a=bl_formula b=bl_formula (WS)* R_PAREN
+bl_implies_operator [Variable current_state]
+ returns [Formula result]:
+
+ (WS)* IMPLIES_OPERATOR_KW
+ a=bl_formula[current_state]
+ b=bl_formula[current_state]
+ (WS)* R_PAREN
+
{
/* TODO */
$result = $a.implies($b);
@@ -197,32 +369,89 @@ bl_implies_operator returns [Formula result]:
;
/**** Computation Tree Logic Expressions **************************************/
-bl_ax_operator returns [Formula result]:
- (WS)* AX_OPERATOR_KW bl_formula (WS)* R_PAREN
+bl_ax_operator [Variable current_state]
+ returns [Formula result]:
+
+ @init
+ {
+ final Variable next_state;
+
+ next_state = VARIABLE_SET.generate_new_state_variable();
+ }
+
+ (WS)* AX_OPERATOR_KW
+ bl_formula[next_state]
+ (WS)* R_PAREN
+
{
/* TODO */
$result =
- $bl_formula.forAll({n | <current_state, n> \in node_connect});
+ $bl_formula.forAll
+ (
+ next_state.in
+ (
+ current_state.join
+ (
+ MODEL.get_predicate_as_relation("node_connect")
+ )
+ );
+ );
}
;
-bl_ex_operator returns [Formula result]:
- (WS)* EX_OPERATOR_KW bl_formula (WS)* R_PAREN
+bl_ex_operator [Variable current_state]
+ returns [Formula result]:
+
+ @init
+ {
+ final Variable next_state;
+
+ next_state = VARIABLE_SET.generate_new_state_variable();
+ }
+
+ (WS)* EX_OPERATOR_KW
+ bl_formula[next_state]
+ (WS)* R_PAREN
+
{
/* TODO */
$result =
- $bl_formula.forSome({n | <current_state, n> \in node_connect});
+ $bl_formula.forSome
+ (
+ next_state.in
+ (
+ current_state.join
+ (
+ MODEL.get_predicate_as_relation("node_connect")
+ )
+ );
+ );
}
;
-bl_ag_operator returns [Formula result]:
- (WS)* AG_OPERATOR_KW bl_formula (WS)* R_PAREN
+
+bl_ag_operator [Variable current_state]
+ returns [Formula result]:
+
+ @init
+ {
+ final Variable next_state;
+
+ next_state = VARIABLE_SET.generate_new_state_variable();
+ }
+
+ (WS)* AG_OPERATOR_KW
+ bl_formula[next_state]
+ (WS)* R_PAREN
+
{
/* TODO */
$result =
- $bl_formula.forSome
+ Formula.replace /* That does not seem to exist. */
(
- current_node
+ next_state,
+ current_state,
+ $bl_formula
).and
(
$bl_formula.forAll