# read_module gm3.rm
read_module gm4.rm

read_spec weak-timeliness.spec

atl_check System_1H weak-timelyP1
atl_check System_2H weak-timelyP2
atl_check System_3H weak-timelyP3 
atl_check System_4H weak-timelyP4