Commit 53836f98 authored by Matthias Simon's avatar Matthias Simon
Browse files

Minor changes

parent b4c87481
Loading
Loading
Loading
Loading
Loading
+13 −17
Original line number Diff line number Diff line
@@ -8,15 +8,15 @@ module InterleaveWithDefault {
		port Port p;
	}

	testcase toplevel() runs on C {
	testcase successfulDefault() runs on C {
		var boolean ok := false;

		p.send(3);
		p.send(4);

		activate(consumeMessage());
		activate(consumeMessage4());

		// the successful default will terminate bellow interleave
		// and continue execution after the block
		// The successful default will terminate bellow interleave
		// and continue execution after the block.
		interleave {
			[] p.receive(1) {
				setverdict(fail);
@@ -35,14 +35,15 @@ module InterleaveWithDefault {
		p.send(1);
		p.send(4);

		activate(consumeMessage());
		activate(consumeMessage4());

		// Message `1` is consumed and interleave is waiting for
		// in first branch for a message 3 or a message 2.
		// Activated default will terminate the nested alt block
		// and will continue is execution of `ok := true`.
		interleave {
			[] p.receive(1) {

				// we are waiting for a message 3 (or a message 2),
				// which never comes.
				// Activated default will terminate `p.receive(3)`
				// and continue execution of the next lone.
				p.receive(3);
				ok := true;
			}
@@ -58,12 +59,7 @@ module InterleaveWithDefault {
		}
	}

	altstep consumeMessage() runs on C {
		p.receive;
	}

	control {
		execute(toplevel(), 10);
		execute(nestedAlt(), 10);
	altstep consumeMessage4() runs on C {
		p.receive(4);
	}
}