diff --git a/Tst/RegressionTests/Feature2Stmts/Correct/pingPongReceive4/pingPongReceive4.p b/Tst/RegressionTests/Feature2Stmts/Correct/pingPongReceive4/pingPongReceive4.p new file mode 100644 index 000000000..203e037ba --- /dev/null +++ b/Tst/RegressionTests/Feature2Stmts/Correct/pingPongReceive4/pingPongReceive4.p @@ -0,0 +1,46 @@ +event ping: (sender: machine, id: int); +event pong: (id: int); + +machine Main { + var follower: machine; + + start state Init { + entry { + var id: int; + follower = new Follower(); + id = 0; + + while(id < 2) { + send follower, ping, (sender=this, id=id); + print format ("(inside) {0}: ping sent", id); + receive { + case pong: (rsp: (id: int)) { + id = rsp.id; + print format ("(inside) {0}: pong received", id); + } + } + print format ("(inside) {0}: done", id); + } + assert (id == 2), format("expected id to be 2, got {0}", id); + + send follower, ping, (sender=this, id=id); + print format ("(outside) {0}: ping sent", id); + receive { + case pong: (rsp: (id: int)) { + id = rsp.id; + print format ("(outside) {0}: pong received", id); + } + } + + assert (id == 3), format("expected id to be 3, got {0}", id); + } + } +} + +machine Follower { + start state Init { + on ping do (payload: (sender: machine, id: int)) { + send payload.sender, pong, (id = payload.id+1,); + } + } +} diff --git a/Tst/RegressionTests/Feature2Stmts/Correct/pingPongReceive5/pingPongReceive5.p b/Tst/RegressionTests/Feature2Stmts/Correct/pingPongReceive5/pingPongReceive5.p new file mode 100644 index 000000000..e11fac2c3 --- /dev/null +++ b/Tst/RegressionTests/Feature2Stmts/Correct/pingPongReceive5/pingPongReceive5.p @@ -0,0 +1,58 @@ +event ping: (sender: machine, id: int); +event pong: (id: int); + +machine Main { + var follower: machine; + + start state Init { + entry { + var id: int; + follower = new Follower(); + id = 0; + + if (id == 0) { + send follower, ping, (sender=this, id=id); + print format ("(first) {0}: ping sent", id); + receive { + case pong: (rsp: (id: int)) { + id = rsp.id*2; + print format ("(first) {0}: pong received", id); + } + } + } + assert (id == 2), format("expected id to be 2, got {0}", id); + + while(id < 4) { + send follower, ping, (sender=this, id=id); + print format ("(inside) {0}: ping sent", id); + receive { + case pong: (rsp: (id: int)) { + id = rsp.id; + print format ("(inside) {0}: pong received", id); + } + } + print format ("(inside) {0}: done", id); + } + assert (id == 4), format("expected id to be 4, got {0}", id); + + send follower, ping, (sender=this, id=id); + print format ("(outside) {0}: ping sent", id); + receive { + case pong: (rsp: (id: int)) { + id = rsp.id; + print format ("(outside) {0}: pong received", id); + } + } + + assert (id == 5), format("expected id to be 5, got {0}", id); + } + } +} + +machine Follower { + start state Init { + on ping do (payload: (sender: machine, id: int)) { + send payload.sender, pong, (id = payload.id+1,); + } + } +} diff --git a/Tst/RegressionTests/Feature2Stmts/DynamicError/pingPongReceive4/pingPongReceive4.p b/Tst/RegressionTests/Feature2Stmts/DynamicError/pingPongReceive4/pingPongReceive4.p new file mode 100644 index 000000000..8404fb142 --- /dev/null +++ b/Tst/RegressionTests/Feature2Stmts/DynamicError/pingPongReceive4/pingPongReceive4.p @@ -0,0 +1,46 @@ +event ping: (sender: machine, id: int); +event pong: (id: int); + +machine Main { + var follower: machine; + + start state Init { + entry { + var id: int; + follower = new Follower(); + id = 0; + + while(id < 2) { + send follower, ping, (sender=this, id=id); + print format ("(inside) {0}: ping sent", id); + receive { + case pong: (rsp: (id: int)) { + id = rsp.id; + print format ("(inside) {0}: pong received", id); + } + } + print format ("(inside) {0}: done", id); + } + assert (id == 2), format("expected id to be 2, got {0}", id); + + send follower, ping, (sender=this, id=id); + print format ("(outside) {0}: ping sent", id); + receive { + case pong: (rsp: (id: int)) { + id = rsp.id; + print format ("(outside) {0}: pong received", id); + } + } + + assert (id != 3), format("expected id to be 3, got {0}", id); // error + } + } +} + +machine Follower { + start state Init { + on ping do (payload: (sender: machine, id: int)) { + send payload.sender, pong, (id = payload.id+1,); + } + } +} diff --git a/Tst/RegressionTests/Feature2Stmts/DynamicError/pingPongReceive5/pingPongReceive5.p b/Tst/RegressionTests/Feature2Stmts/DynamicError/pingPongReceive5/pingPongReceive5.p new file mode 100644 index 000000000..a8da85d04 --- /dev/null +++ b/Tst/RegressionTests/Feature2Stmts/DynamicError/pingPongReceive5/pingPongReceive5.p @@ -0,0 +1,58 @@ +event ping: (sender: machine, id: int); +event pong: (id: int); + +machine Main { + var follower: machine; + + start state Init { + entry { + var id: int; + follower = new Follower(); + id = 0; + + if (id == 0) { + send follower, ping, (sender=this, id=id); + print format ("(first) {0}: ping sent", id); + receive { + case pong: (rsp: (id: int)) { + id = rsp.id*2; + print format ("(first) {0}: pong received", id); + } + } + } + assert (id == 2), format("expected id to be 2, got {0}", id); + + while(id < 4) { + send follower, ping, (sender=this, id=id); + print format ("(inside) {0}: ping sent", id); + receive { + case pong: (rsp: (id: int)) { + id = rsp.id; + print format ("(inside) {0}: pong received", id); + } + } + print format ("(inside) {0}: done", id); + } + assert (id == 4), format("expected id to be 4, got {0}", id); + + send follower, ping, (sender=this, id=id); + print format ("(outside) {0}: ping sent", id); + receive { + case pong: (rsp: (id: int)) { + id = rsp.id; + print format ("(outside) {0}: pong received", id); + } + } + + assert (id != 5), format("expected id to be 5, got {0}", id); // error + } + } +} + +machine Follower { + start state Init { + on ping do (payload: (sender: machine, id: int)) { + send payload.sender, pong, (id = payload.id+1,); + } + } +}