Verification

There is also the possibility of manual verifying an actor’s behavior. A state machine must be defined for an actor, which defines states and transitions. It can be defined as ingoing and outgoing transitions as well. An actor must implement the interface ActorVerification. This interface defines a method called to verify, which returns a verification state machine. The corresponding actor’s transitions of this state machine can then be verified by the ActorVerificator. The verificator can find cycles, unreachable or dead states (with no more outgoing transition(s), it hangs on that state). Furthermore, there is also the possibility of interconnecting all state machines of all actors in the system and verifying the whole system. This verification in the current state verifies only predefined declared transition states. In the future, it would be good to have the option to test this against an in-production running actor system so that the actor system can be verified in real-time (to check if the system behaves as it should).

Example

At the verification example, the ping actor has the following states defined: PING, A, B, C, D. The transitions are PING→D, A→B, B→C, C→A (the last four transitions with ingoing event zero), PING[event:PONG]→PING (with ingoing PONG event) and PING→PING[event:PING] (with outgoing PING event to the pong actor). The initial state is PING. The pong actor has only one state, PONG, and the transitions PONG[event:PING]→PONG (with ingoing PING event) and PONG→PONG [event:PONG] (with outgoing PONG event to the ping actor) are defined. The overall result of the verification process is:

• Cycles: [pong-actor:PONG], [ping-actor:PING, pong-actor:PONG], [ping-actor:PING], [ping-actor:C, ping-actor:B, ping-actor:A]
• Unreachables: [ping-actor:A, ping-actor:C, ping-actor:B]
• Deads: [ping-actor:D].

// Snippet from the ping actor
@Override
public ActorVerificationSM verify() {
	ActorVerificationSM result = new ActorVerificationSM(this);
	result
		.addInitialStateMarker("PING")
		.addInTransition("PING", "PING", PONG)
		.addOutTransition("PING", "PING", PING, "pong")
			
		.addStateMarker("D")
		.addInTransition("PING", "D", 0)
			
		.addStateMarker("A")
		.addStateMarker("B")
		.addStateMarker("C")
		.addInTransition("A", "B", 0)
		.addInTransition("B", "C", 0)
		.addInTransition("C", "A", 0);
			
	return result;
}
// Snippet from the pong actor
@Override
public ActorVerificationSM verify() {
	ActorVerificationSM result = new ActorVerificationSM(this);
	result
		.addInitialStateMarker("PONG")
		.addInTransition("PONG", "PONG", PING)
		.addOutTransition("PONG", "PONG", PONG, "ping");
			
	return result;
}
/* Full examples under https://github.com/relvaner/actor4j/tree/master/actor4j-examples */