Rule table
The five rules of the Generic Application: each in English, as the AI wrote it in logic, what it restricts, which safety properties need it, and what happens without it.
With all five rules in force, 6 of 7 safety properties hold. Needed for lists the properties that hold with all five rules and fail without this one; Without it is Foras's verdict on the other four. Each is proved, and checked by brute force.
| Rule | In English, and the AI's reading | As logic (the AI's clauses) | Restricts | Needed for | Alone | Without it |
|---|---|---|---|---|---|---|
| GA-1 | A signal only clears when the section its train is about to enter is empty.I read 'the section its train is about to enter' as the first section past the signal: s_main for S1 (blue), and s_east for S2 (green) and S3 (silver). 'Empty' means no other train is on that section at that moment; silver can never be on s_main, so S1 only checks green. The rule checks nothing further along the route and does not mention the points, so throw is unrestricted. | -not_main(x2) | r1_clear_s1(st(x1,x2,x3,x4,x5,x6,x7)). -not_east(x1) | -not_east(x3) | r1_clear_s2(st(x1,x2,x3,x4,x5,x6,x7)). -not_east(x1) | -not_east(x2) | r1_clear_s3(st(x1,x2,x3,x4,x5,x6,x7)). |
clear S1, clear S2, clear S3 | P1 | crash in 4 moves | crash in 5 moves |
| GA-2 | Two trains whose routes share a section never hold a green at the same time.Every pair of routes shares s_east, so I read the rule as: a signal may be cleared only while the other two signals are red. 'Holding a green' means the signal itself is green, so trains already past their signal (now red) are not considered, and throwing the points is not restricted. | r2_clear_s1(st(x1,x2,x3,x4,red,red,x7)). r2_clear_s2(st(x1,x2,x3,red,x5,red,x7)). r2_clear_s3(st(x1,x2,x3,red,red,x6,x7)). |
clear S1, clear S2, clear S3 | P1, P2 | crash in 4 moves | crash in 5 moves |
| GA-3 | Once any train has a green, the points stay where they are until it is through.The rule restricts only throw: it is allowed only when no signal is green and no train is on its way, since every moving train got there by passing a green. I read "through" as the train having finished its run (waiting, arrived, stuck in the siding or gone, per the still_ helpers), not merely past the points; clearing signals is left unrestricted. | -still_b(x1) | -still_o(x2) | -still_s(x3) | r3_throw(st(x1,x2,x3,red,red,red,x7)). |
throw the points | P1, P3, P5 | crash in 5 moves | crash in 4 moves |
| GA-4 | Never clear a signal while another train is still on its way.I read 'another train' as either of the two trains other than the one waiting at the signal being cleared, and 'on its way' as not satisfying the matching still_ helper. So a train behind a green signal that has not yet moved counts as not on its way. The rule restricts only clear_s1, clear_s2 and clear_s3; throw is unrestricted. | -still_o(x2) | -still_s(x3) | r4_clear_s1(st(x1,x2,x3,x4,x5,x6,x7)). -still_b(x1) | -still_s(x3) | r4_clear_s2(st(x1,x2,x3,x4,x5,x6,x7)). -still_b(x1) | -still_o(x2) | r4_clear_s3(st(x1,x2,x3,x4,x5,x6,x7)). |
clear S1, clear S2, clear S3 | P1 | crash in 4 moves | crash in 5 moves |
| GA-5 | Only clear the regional's signal when the points are set for the platform.I read 'the regional's signal' as S2 and 'set for the platform' as Points = nrm. The rule restricts only clear_s2, with no other conditions. It does not forbid throwing the points after S2 is cleared, and it does not check where blue or silver are. | r5_clear_s2(st(x1,x2,x3,x4,x5,x6,nrm)). |
clear S2 | P1, P5 | crash in 4 moves | crash in 4 moves |
Try them in the simulator Verification report, all five rules