Falls ein Programm nur einen einzigen next-Shadow enthält, dann kann man den trotzdem nicht deaktivieren; er könnte ja in einer Schleife liegen.
Das habe ich gemeint
Wie wäre denn die Antwort auf dei Klausurfrage zu 3. c)?
Es ist mir klar, dass OSA nicht ausschließen kann, dass ein next in den Endzustand fürt, allerdings ist mir nicht ganz klar warum bzw. wie man es begründen sollte.
So wie ich das verstanden habe, überprüft OSA ohnehin das selbe wie der Quick Check. Also ob ein Shadow vokommt, der den Automaten in den Endzustand bringen würde. Allerdings mit Beachtung, dass ein shadow auf unterschiedlichen Objekten arbeiten könnte.
Hat man jetzt ein Programm, indem der "next"-Shadow vorkommt, ist es eigentlich egal ob sich dieser nun auf ein oder mehrere Objekte bezieht, da man in keinem fall sagen kann ob next in den Endzustand fürt oder nicht.