Simplify synthesized supervisor wrt. state plant invariant guards.
In issue #107 (closed), we add state plant invariants to data-based synthesis. We do that by encoding the state plant invariants in the guards of the edges (by applying the edge update backward on the state plant invariant). Basically, we add guards to edges such that edges to states that violate state plant invariants cannot be taken. As a result, the resulting supervisor may contain guards that arise from the state plant invariants. Since the plant already enforces that edges to states that violate the state plant invariants are never taken, the supervisor does not need to enforce that. Hence, it should be possible to simplify the resulting supervisor wrt. these guards.
Solution direction:
- In
applyStatePlantInvs
saveupdPred
, that is the state plant invariant guard for that edge. - Combine the
updPred
's for different edges for the same event. - Simplify the linearized edges wrt. the combined
updPred
's.
My initial guess is that for step 2 we need to include the original automaton guards, as well. Otherwise, we won't know to which edge an updPred
belongs. We have to make sure that a state plant invariant guard that belongs to one edge doesn't simplify another edge.
Ideally, I would like to use an updPred
to simplify a synthesis edge. Instead of combining updPred
's to simplify the linearized edges. However, I don't think that fits the current framework.