Incompatible predicates in session_core
In the B machine session_core.mch
, we have the definitions:
d_typing ==
s_session <: t_session &
a_state : s_session --> t_sessionState & // a session shall be associated to a state
...
and
d_close_session (session) ==
s_session := s_session - {session} || // If session was valid session, remove it
...
a_state(session) := e_session_closed || // keep session token as used
...
These are clearly incompatible, because the latter will not keep the domain of a_state
equal to s_session
.
I do not know which one is right.