% Once a job has been killed, it cannot resurrect and start running. (safety)
% The property fails, as exemplified by the trace noZombieJobs.trc
%
% Currently (December 2011), verifying the property using pbes2bool or pbes2bes requires
% too much time (> 50 hours) and is very memory-hungry. The violation can be detected
% much faster by specifying a monitor process and searching for the presence of an action 
% using lps2lts.

[true*.state([jobstatus(Killed,MarkedForTermination)]). true*. state([jobstatus(Checking,JobScheduling)]) ]false
