This issue concerns model checking only when using variably-typed partitions with the library entry point (SynopticLib).
During model checking, if for example we're traversing a state machine corresponding to AFby, we enter an aSeen state when we see A from the aNotSeen state, etc. Because we're traversing a graph during model checking, we theoretically have a different such state machine for each possible path through the model, and we implement this by simply keeping one state machine where we're simultaneously in all states that any of those individual state machines would be in. Thus, if we see A when we're in both aNotSeen and aThenNonBSeen, we're now in aSeen and (still) aThenNonBSeen.
Think more about how variable partitions affect this process and ultimately if the current strategy is good enough for variably-typed model checking to remain correct? We already consider all possible next states in the combined state machine described above, i.e., we don't short-circuit when we see A and assume we can't also see B in this partition. However, we need to verify that there is no possible odd behavior due to a partition containing both A and B.
Specifically, draft new model checking state machines for each invariant that has one or more states that consider A and B being seen in the same partition. Then for each, think about whether this state is simply redundant or whether it actually is necessary. If the latter, augment the model checking state machines in code.
This issue concerns model checking only when using variably-typed partitions with the library entry point (SynopticLib).
During model checking, if for example we're traversing a state machine corresponding to AFby, we enter an aSeen state when we see A from the aNotSeen state, etc. Because we're traversing a graph during model checking, we theoretically have a different such state machine for each possible path through the model, and we implement this by simply keeping one state machine where we're simultaneously in all states that any of those individual state machines would be in. Thus, if we see A when we're in both aNotSeen and aThenNonBSeen, we're now in aSeen and (still) aThenNonBSeen.
Think more about how variable partitions affect this process and ultimately if the current strategy is good enough for variably-typed model checking to remain correct? We already consider all possible next states in the combined state machine described above, i.e., we don't short-circuit when we see A and assume we can't also see B in this partition. However, we need to verify that there is no possible odd behavior due to a partition containing both A and B.
Specifically, draft new model checking state machines for each invariant that has one or more states that consider A and B being seen in the same partition. Then for each, think about whether this state is simply redundant or whether it actually is necessary. If the latter, augment the model checking state machines in code.