Semantics of send to halted machines

[rajivr]

I am new to P language and am still working through the tutorials.

I was trying to get a better sense of send semantics, and it looks to me send is always successful , irrespective of whether the target machine is in a halted or non-halted state.

I used the following example.

event eHello;

event eShutdown;

event eActivateMachineB;

machine MachineA {
    start state Init {
        on eHello do {
            print("received eHello");
        }

        on eShutdown do {
            print("received eShutdown. shuttting down...");
            raise halt;
        }
    }
}

machine MachineB {
    var machine_a: MachineA;

    start state Init {
        entry (m: MachineA) {
            machine_a = m;

            goto WaitForRequests;
        }
    }

    state WaitForRequests {
        on eActivateMachineB do {
            send machine_a, eHello;

            send machine_a, eShutdown;

            send machine_a, eHello;

            send machine_a, eHello;
        }
    }
}

machine MachineBDriver {
    var m_a: MachineA;
    var m_b: MachineB;

    start state Init {
        entry {
            m_a = new MachineA();

            m_b = new MachineB(m_a);

            send m_b, eActivateMachineB;

            goto WaitForRequests;
        }
    }

    state WaitForRequests {

    }
}

test tcMachineBDriver [main = MachineBDriver]:
    {
        MachineA,
        MachineB,
        MachineBDriver
    };

When I attempted to run it, I noticed

1. It showed Found 0 bugs.

2. It threw and automatically handled UnhandledEventException (essentially ignoring the exception)

This behavior leads me to infer that send to halted machines would not result in errors. Is my understanding correct?

$ p check -s 1 -v
.. Searching for a P compiled file locally in folder ./PGenerated/
.. Found a P compiled file: ./PGenerated/CSharp/net8.0/FailureDetector.dll
.. Checking ./PGenerated/CSharp/net8.0/FailureDetector.dll
.. Test case :: tcMachineBDriver
... Checker is using 'random' strategy (seed:1388482806).
..... Schedule #1
<TestLog> Running test 'tcMachineBDriver'.
<CreateLog> MachineBDriver(1) was created by task '2'.
<StateLog> MachineBDriver(1) enters state 'Init'.

...

<DequeueLog> 'MachineA(2)' dequeued event 'eShutdown' in state 'Init'.
<PrintLog> received eShutdown. shuttting down...
<RaiseLog> 'MachineA(2)' raised event 'PHalt' in state 'Init'.
<StateLog> MachineA(2) exits state 'Init'.
<PopLog> MachineA(2) popped state Init due to unhandled event 'PHalt'.
<ExceptionLog> MachineA(2) running action '' in state 'Init' threw exception 'UnhandledEventException'.
<ExceptionLog> MachineA(2) running action '' in state 'Init' chose to handle exception 'UnhandledEventException'.
<HaltLog> MachineA(2) halted with 2 events in its inbox.
... Emitting verbose logs:
..... Writing PCheckerOutput/BugFinding/FailureDetector_0_verbose.trace.json
... ### Process 0 is terminating
... Emitting coverage report:
..... Writing PCheckerOutput/BugFinding/FailureDetector.coverage.txt
..... Writing PCheckerOutput/BugFinding/FailureDetector.sci
... Checking statistics:
..... Found 0 bugs.
... Scheduling statistics:
..... Explored 1 schedule
..... Explored 1 timeline
..... Number of scheduling points in terminating schedules: 14 (min), 14 (avg), 14 (max).
..... Writing PCheckerOutput/BugFinding/FailureDetector_pchecker_summary.txt
... Elapsed 0.2340504 sec.
. Done
~~ [PTool]: Thanks for using P! ~~

[ankushdesai]

Yes, you are absolutely right, sends to halted machines are similar to no-op; basically the message is dropped by the network ....