find a way to deal with input-output non-determinism
|Status:||New||Start date:||22 May 2009|
when we are in a state where we can both apply stimulus and make an observation, and the model does not have a buffer for the outputs, we have a problem, because in the model it looks like we disable the output observation by doing the input transition, but in the real program the output is given anyway - i.e. the model is wrong.
but can we somehow automatically add queue contexts for the model?