summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--cfg-to-paths/src/Main.java2
-rw-r--r--instr-to-kodkod/parser/PropertyParser.g4252
2 files changed, 188 insertions, 66 deletions
diff --git a/cfg-to-paths/src/Main.java b/cfg-to-paths/src/Main.java
index 481d53f..853983a 100644
--- a/cfg-to-paths/src/Main.java
+++ b/cfg-to-paths/src/Main.java
@@ -97,7 +97,7 @@ public class Main
out.write("(add_element path " + id + ")\n");
out.write("(is_path_of " + id + " " + tuple.get(0) + ")\n");
- for (int i = 1; i < tuple_size; ++i)
+ for (int i = 0; i < tuple_size; ++i)
{
out.write("(contains_node " + id + " " + tuple.get(i) + ")\n");
diff --git a/instr-to-kodkod/parser/PropertyParser.g4 b/instr-to-kodkod/parser/PropertyParser.g4
index 2df87cb..4aeeffc 100644
--- a/instr-to-kodkod/parser/PropertyParser.g4
+++ b/instr-to-kodkod/parser/PropertyParser.g4
@@ -18,6 +18,7 @@ options
@members
{
/* of the class */
+
}
prog:
@@ -429,7 +430,6 @@ bl_ex_operator [Variable current_state]
}
;
-
bl_ag_operator [Variable current_state]
returns [Formula result]:
@@ -447,135 +447,257 @@ bl_ag_operator [Variable current_state]
{
/* TODO */
$result =
- Formula.replace /* That does not seem to exist. */
- (
- next_state,
- current_state,
- $bl_formula
- ).and
+ $bl_formula.forAll
(
- $bl_formula.forAll
- (
- {n | <p, n> \in contains_node}
- ).forAll
+ next_state.in
(
- {p | <p, current_node> \in is_path_of}
+ current_state.join
+ (
+ MODEL.get_predicate_as_relation
+ (
+ "is_path_of"
+ ).transpose() /* (is_path_of path node), we want the path. */
+ ).join
+ (
+ MODEL.get_predicate_as_relation("contains_node")
+ ).
)
)
}
;
-bl_eg_operator returns [Formula result]:
- (WS)* EG_OPERATOR_KW bl_formula (WS)* R_PAREN
+bl_eg_operator [Variable current_state]
+ returns [Formula result]:
+
+ @init
+ {
+ final Variable next_state, chosen_path;
+
+ next_state = VARIABLE_SET.generate_new_state_variable();
+ chosen_path = VARIABLE_SET.generate_new_state_variable();
+ }
+
+ (WS)* EG_OPERATOR_KW
+ bl_formula[next_state]
+ (WS)* R_PAREN
+
{
/* TODO */
$result =
- $bl_formula.forSome
- (
- current_node
- ).and
+ $bl_formula.forAll
(
- $bl_formula.forSome
+ next_state.in
(
- {n | <p, n> \in contains_node}
- ).forAll
+ chosen_path.join
+ (
+ MODEL.get_predicate_as_relation("contains_node")
+ ).
+ )
+ ).forSome
+ (
+ chosen_path.in
(
- {p | <p, current_node> \in is_path_of}
+ current_state.join
+ (
+ MODEL.get_predicate_as_relation
+ (
+ "is_path_of"
+ ).transpose() /* (is_path_of path node), we want the path. */
+ )
)
);
}
;
-bl_af_operator returns [Formula result]:
- (WS)* AF_OPERATOR_KW bl_formula (WS)* R_PAREN
+bl_af_operator [Variable current_state]
+ returns [Formula result]:
+
+ @init
+ {
+ final Variable next_state, chosen_path;
+
+ next_state = VARIABLE_SET.generate_new_state_variable();
+ chosen_path = VARIABLE_SET.generate_new_state_variable();
+ }
+
+ (WS)* AF_OPERATOR_KW
+ bl_formula[next_state]
+ (WS)* R_PAREN
+
{
/* TODO */
$result =
$bl_formula.forSome
(
- current_node
- ).or
- (
- $bl_formula.forAll
+ next_state.in
(
- {n | <p, n> \in contains_node}
- ).forSome
+ chosen_path.join
+ (
+ MODEL.get_predicate_as_relation("contains_node")
+ ).
+ )
+ ).forAll
+ (
+ chosen_path.in
(
- {p | <p, current_node> \in is_path_of}
+ current_state.join
+ (
+ MODEL.get_predicate_as_relation
+ (
+ "is_path_of"
+ ).transpose() /* (is_path_of path node), we want the path. */
+ )
)
);
}
;
-bl_ef_operator returns [Formula result]:
- (WS)* EF_OPERATOR_KW bl_formula (WS)* R_PAREN
+bl_ef_operator [Variable current_state]
+ returns [Formula result]:
+
+ @init
+ {
+ final Variable next_state, chosen_path;
+
+ next_state = VARIABLE_SET.generate_new_state_variable();
+ chosen_path = VARIABLE_SET.generate_new_state_variable();
+ }
+
+ (WS)* EF_OPERATOR_KW
+ bl_formula[next_state]
+ (WS)* R_PAREN
+
{
/* TODO */
$result =
$bl_formula.forSome
(
- current_node
- ).or
- (
- $bl_formula.forSome
+ next_state.in
(
- {n | <p, n> \in contains_node}
- ).forSome
+ chosen_path.join
+ (
+ MODEL.get_predicate_as_relation("contains_node")
+ ).
+ )
+ ).forSome
+ (
+ chosen_path.in
(
- {p | <p, current_node> \in is_path_of}
+ current_state.join
+ (
+ MODEL.get_predicate_as_relation
+ (
+ "is_path_of"
+ ).transpose() /* (is_path_of path node), we want the path. */
+ )
)
);
}
;
-bl_au_operator returns [Formula result]: (WS)* AU_OPERATOR_KW f1=bl_formula f2=bl_formula (WS)* R_PAREN
+bl_au_operator [Variable current_state]
+ returns [Formula result]:
+
+ @init
+ {
+ final Variable f1_state, f2_state, chosen_path;
+
+ f1_state = VARIABLE_SET.generate_new_state_variable();
+ f2_state = VARIABLE_SET.generate_new_state_variable();
+ chosen_path = VARIABLE_SET.generate_new_state_variable();
+ }
+
+ (WS)* AU_OPERATOR_KW
+ f1=bl_formula[f1_state]
+ f2=bl_formula[f2_state]
+ (WS)* R_PAREN
+
{
/* TODO */
$result =
- $f1.forSome
+ $f1.forAll
(
- current_node
- ).and
- (
- $f2.and
+ f1_state.in
(
- $f1.forAll
+ f2_state.join
(
- {t | <p, t, n> \in is_before}
+ chosen_path.join
+ (
+ MODEL.get_predicate_as_relation("is_before")
+ ).transpose()
)
- ).forSome
+ );
+ ).forSome
+ (
+ f2_state.in
(
- {n | <p, n> \in contains_node}
- ).forAll
+ chosen_path.join
+ (
+ MODEL.get_predicate_as_relation("contains_node")
+ )
+ )
+ ).forAll
+ (
+ chosen_path.in
(
- {p | <p, current_node> \in is_path_of}
+ current_state.join
+ (
+ MODEL.get_predicate_as_relation("is_path_of").transpose()
+ )
)
);
}
;
-bl_eu_operator returns [Formula result]:
- (WS)* EU_OPERATOR_KW f1=bl_formula f2=bl_formula (WS)* R_PAREN
+bl_eu_operator [Variable current_state]
+ returns [Formula result]:
+
+ @init
+ {
+ final Variable f1_state, f2_state, chosen_path;
+
+ f1_state = VARIABLE_SET.generate_new_state_variable();
+ f2_state = VARIABLE_SET.generate_new_state_variable();
+ chosen_path = VARIABLE_SET.generate_new_state_variable();
+ }
+
+ (WS)* EU_OPERATOR_KW
+ f1=bl_formula[f1_state]
+ f2=bl_formula[f2_state]
+ (WS)* R_PAREN
+
{
/* TODO */
$result =
- $f1.forSome
- (
- current_node
- ).and
+ $f1.forAll
(
- $f2.and
+ f1_state.in
(
- $f1.forAll
+ f2_state.join
(
- {t | <p, t, n> \in is_before}
+ chosen_path.join
+ (
+ MODEL.get_predicate_as_relation("is_before")
+ ).transpose()
)
- ).forSome
+ );
+ ).forSome
+ (
+ f2_state.in
(
- {n | <p, n> \in contains_node}
- ).forSome
+ chosen_path.join
+ (
+ MODEL.get_predicate_as_relation("contains_node")
+ )
+ )
+ ).forSome
+ (
+ chosen_path.in
(
- {p | <p, current_node> \in is_path_of}
+ current_state.join
+ (
+ MODEL.get_predicate_as_relation("is_path_of").transpose()
+ )
)
);
}