I read his article, and I make his spec by my self.
He wrote the following:
But why this error message? It turns out that our model only describes the steps up to this point. Once the trains have reached their destinations, they will not move any more. Nothing happens at all. A classical deadlock.
I don’t want to extend the model to let the trains go on and on and on, because we would never finish this exercise. So I decide to remove the check for the deadlock so hopefully no other error will be found…
Not quite yet. TLC reports another stuttering step. Here train 2 advances up to track 3 and train 1 is still on track 1. Instead of train one progressing, switch 1 keeps changing its state forever. Seems like the dispatcher in our interlocking can’t make up his mind.
And I find a way to terminate.
what
feat(TrainSiding): make specs
feat(TrainSiding): let to terminate
What not to do
To implement the way to change switches by arbitrary way(The trains are yet designed to go by the designed track)
To model the real cases:
To implement constants, in order to make any models.
why
Stefan provides us one of the good example.
https://www.heinbockel.eu/2019/12/08/train-sidings-a-tla-example/
I read his article, and I make his spec by my self.
He wrote the following:
And I find a way to terminate.
what
What not to do