Skip to content
Snippets Groups Projects
Commit 08736cf6 authored by Jan Gruteser's avatar Jan Gruteser
Browse files

adapt translation of SubSeq

parent 6f14b439
Branches
Tags
No related merge requests found
Pipeline #148723 failed
...@@ -953,36 +953,44 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals, BBuil ...@@ -953,36 +953,44 @@ public class BAstCreator extends BuiltInOPs implements TranslationGlobals, BBuil
break; break;
case B_OPCODE_subseq: { // SubSeq(s,a,b) case B_OPCODE_subseq: { // SubSeq(s,a,b)
// %p.(p : 1..(b-a+1)| s(p+a-1)) // new translation: (s /|\ b) \|/ a-1 (this saves us a new identifier name)
ALambdaExpression lambda = new ALambdaExpression(); returnNode = new ARestrictTailExpression(
lambda.setIdentifiers(createIdentifierList("t_")); new ARestrictFrontExpression(
AMemberPredicate member = new AMemberPredicate(); visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]), // s
member.setLeft(createIdentifierNode("t_")); visitExprOrOpArgNodeExpression(opApplNode.getArgs()[2]) // b
AIntervalExpression interval = new AIntervalExpression(); ),
interval.setLeftBorder(new AIntegerExpression(new TIntegerLiteral("1"))); new AMinusOrSetSubtractExpression(
AMinusOrSetSubtractExpression minus = new AMinusOrSetSubtractExpression(); visitExprOrOpArgNodeExpression(opApplNode.getArgs()[1]), // a
minus.setLeft(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[2])); createIntegerNode("1")
minus.setRight(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[1])); )
AAddExpression add = new AAddExpression(); );
add.setLeft(minus);
add.setRight(new AIntegerExpression(new TIntegerLiteral("1")));
interval.setRightBorder(add);
member.setRight(interval);
lambda.setPredicate(member);
AAddExpression add2 = new AAddExpression();
add2.setLeft(createIdentifierNode("t_"));
add2.setRight(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[1]));
AMinusOrSetSubtractExpression minus2 = new AMinusOrSetSubtractExpression();
minus2.setLeft(add2);
minus2.setRight(new AIntegerExpression(new TIntegerLiteral("1")));
ArrayList<PExpression> params = new ArrayList<>();
params.add(minus2);
AFunctionExpression func = new AFunctionExpression();
func.setIdentifier(visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]));
func.setParameters(params);
lambda.setExpression(func);
returnNode = lambda;
break; break;
// previous translation: %t_.(t_ : 1..(b-a+1)| s(t_+a-1))
/*PExpression a = visitExprOrOpArgNodeExpression(opApplNode.getArgs()[1]);
PExpression b = visitExprOrOpArgNodeExpression(opApplNode.getArgs()[2]);
returnNode = new ALambdaExpression( // %t_.(t_ : 1..(b-a+1)| s(t_+a-1))
createIdentifierList("t_"),
new AMemberPredicate( // t_ : 1..(b-a+1)
createIdentifierNode("t_"),
new AIntervalExpression(
createIntegerNode("1"),
new AAddExpression(
new AMinusOrSetSubtractExpression(b, a),
createIntegerNode("1")
)
)
),
new AFunctionExpression( // s(t_+a-1)
visitExprOrOpArgNodeExpression(opApplNode.getArgs()[0]), // s
Collections.singletonList(
new AMinusOrSetSubtractExpression(
new AAddExpression(createIdentifierNode("t_"), a.clone()),
createIntegerNode("1")
)
)
)
);*/
} }
case B_OPCODE_assert: { case B_OPCODE_assert: {
......
...@@ -86,7 +86,9 @@ public class SequencesTest { ...@@ -86,7 +86,9 @@ public class SequencesTest {
+ "ASSUME SubSeq(<<1,2,3,4,5>>, 2, 3) = <<2,3>> \n" + "ASSUME SubSeq(<<1,2,3,4,5>>, 2, 3) = <<2,3>> \n"
+ "================================="; + "=================================";
final String expected = "MACHINE Testing\n" final String expected = "MACHINE Testing\n"
+ "PROPERTIES %(t_).(t_ : 1 .. (3 - 2) + 1 | [1,2,3,4,5](((t_ + 2) - 1))) = [2,3] \n" // + "PROPERTIES %(t_).(t_ : 1 .. (3 - 2) + 1 | [1,2,3,4,5](((t_ + 2) - 1))) = [2,3] \n"
// new translation:
+ "PROPERTIES ([1,2,3,4,5] /|\\ 3) \\|/ (2 - 1) = [2,3] \n"
+ "END"; + "END";
compare(expected, module); compare(expected, module);
} }
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment