1 2 3 4
\* Direct-TLC check for SYS-0024 startup init-gating (safety). \* Run from specs/: java -jar tla2tools.jar -config InitGateModel.cfg InitGateModel.tla SPECIFICATION GateSpec INVARIANT MutationsGatedByInit