/************************************************************* -- Railroad Gate Controller -- -- Model described in -- "Parametric Real-Time Reasoning" (fig. 2) -- Alur, Henzinger, Vardi (STOC 1993) -- -- Etienne ANDRE -- Laboratoire d'Informatique de Paris Nord -- -- Created : 2011/11/25 -- Last modified : 2012/01/07 *************************************************************/ parameter a; parameter b; parameter c; parameter d; parameter e; parameter f; Train = approach -> ((Wait[a]; in -> out -> exit -> Skip) within[b]); Train; Gate = lower -> ((Wait[c]; down -> Skip) within[d]); raise -> ((Wait[c]; up -> Skip) within[d]); Gate; Controller = approach -> ((Wait[e]; lower -> Skip) within[f]); exit -> ((Wait[e]; raise -> Skip) within[f]); Controller; System = Train || Gate || Controller; #assert System deadlockfree; #synthesize System with a = 4, b = 6, c = 1, d = 2, e = 2, f = 3 ; #synthesize System reachesall;