Every state and transition could be typed and a model can teach DMC the type. This way, information such as whether or not a state is erroneous, can be easily extracted. Or DMC can be taught the name of global variables. The type could bring meaning to every location of each state in the DAG of states that form a state.
Potentially, this should allow to hide transitions/states in such a way that the state space can be made smaller. For example, we might want to only print transitions/states where certain global variables change. This might be achievable with a separate module that implements the DMC API on two sides, as a wrapper around a model.
Every state and transition could be typed and a model can teach DMC the type. This way, information such as whether or not a state is erroneous, can be easily extracted. Or DMC can be taught the name of global variables. The type could bring meaning to every location of each state in the DAG of states that form a state.
Potentially, this should allow to hide transitions/states in such a way that the state space can be made smaller. For example, we might want to only print transitions/states where certain global variables change. This might be achievable with a separate module that implements the DMC API on two sides, as a wrapper around a model.