We have a separate logon relation testing whether we are not logged on. We get an uncommitted output – why, why not false?
We force the new Logon relation True, which causes the other logon to output a True, which negates the existential state. We need to interpose something which handles the inconsistency.
This suggests we should have separate relations for "he logged on" – the action – and "he is logged on" – the state, in the way that "someone starts running", where the start relation initiates the running state, and can have whatever detail is required – "he took a week to start running". When the person logs on successfully, the state is created, or it is reinitiated if it is already there. The state is terminated by logging off. The inconsistency is avoided, as the ToLogOn action is initiated by the incoming propositional True, changes the state, but does not radiate a True existential state before altering any external IsLoggedOn state. The incoming False existential state disables the True propositional state – more exactly, it bounds it in time.
If the state had not been present, it would have been created.
The IsLoggedOn state will be terminated by a ToLogOff (which will, in turn, create an IsLoggedOff state).
The result is
We need to be able to specify whether the start or finish of the action sets the state.