CryptoPatrick / labs

Labs/RailCheck

Make the station safe

Select the rules the railway dispatcher must follow; Artificial Intelligence translates each rule to logic. Next, the theorem prover Foras, attempts to verify every order of moves that the rules allow. The simulation exposes any dangerous moves that the set of rules allow.

  1. You choose the rules
  2. AI converts rules into logic
  3. Foras verifies the logic
  4. Simulation exposes dangerous logic
3 trains · 5 sections
No rules
Platform Points West approach Main line Siding Single line East approach To the east → S1 S3 S2 blue green silver

Verification

Remember: once you're done experimenting with rules, apply them to the Groningen Network!

The Rules

Switch rules on or off. Foras checks all the rules that are on together, then shows the verdict and the board.

The Logic

Compare each line with its rule in English. An AI wrote it once and it never changes, so a flaw in the wording stays here. 

    


    

      

        
The Verdict

        Read the verdict for the rules that are on. Press Play or Step on the board to watch the moves listed here: the crash, or a safe way home. After a crash, switch on the rule named under "Would have stopped it".
      

      

      
    
      
    
      
    Foras 0.4.0 · Every answer cross-checked by an independent brute-force search.
    
    
    
    

    
  
    
  
    
  
    
    
    
    
      
    Route Table
    
      
    Derived from the layout, not typed: for each signal, the route it protects, the sections and points that route needs, and the routes it must never run with.
    
      
    
      
    
    
    
    
    
      
    Safety Properties
    
      
    The collision is one property of seven. Each is proved on its own for the rules ticked above; a violation is a trace you can replay on the board.
    
      
    
      
    
      
    Verification report
    
    
    
    
    
      
    Interlocking Code
    
      
    The rules checked above define the interlocking’s command permissions. Each command was generated from a single expression, compiled, and verified against the clauses Foras proved. We offer three different representations of the interlocking code, and each can be downloaded 
    
      
    
        
    
          
          
          
        
    
        
    
      
    
      
    Download