> Presumably switches already report their position to somewhere.
Yeah and this somewhere already knows whether a crash is going to happen. In which case your solution brings no benefit. You can't rely on the correctness of a system, which you want to make an alternative to, to help in the case the original system fails.
This discussion focuses on a non-problem (granted partly due to an imprecise comment of mine). The system knows where all the trains are and also that a crash will happen, if the decision is made, that then indeed was made.
What is needed is that the system needs to convince the operator there is still a problem, after it proved itself unreliable. My suggestion would be a log of the constraints the prover encountered while determining whether there is a conflict. This certainly already exists somewhere in the background, but I am not aware whether that is currently shown to operators in deployed systems. It does exist somewhat in the research systems we use in university.
Yeah and this somewhere already knows whether a crash is going to happen. In which case your solution brings no benefit. You can't rely on the correctness of a system, which you want to make an alternative to, to help in the case the original system fails.
This discussion focuses on a non-problem (granted partly due to an imprecise comment of mine). The system knows where all the trains are and also that a crash will happen, if the decision is made, that then indeed was made.
What is needed is that the system needs to convince the operator there is still a problem, after it proved itself unreliable. My suggestion would be a log of the constraints the prover encountered while determining whether there is a conflict. This certainly already exists somewhere in the background, but I am not aware whether that is currently shown to operators in deployed systems. It does exist somewhat in the research systems we use in university.