read_module gm3opt.rm
read_spec abuse-freeness-gm-3-opt.spec

atl_check System_3H not-abuse-freeness-P3-opt