#------------------------------------------------------------------------------
# Basic version
#------------------------------------------------------------------------------

# first compute optimal expected time and export digital clocks MDP
prism scheduler.prism scheduler.props -prop 2 -ptamethod digital -exportdigital digital.prism

# next compute optimal scheduler for expected time (from MDP)
prism digital.prism scheduler.props -prop 2 -exportadvmdp adv.tra -exportstates adv.sta -exportlabels adv.lab -exporttransrewards adv.rew

# finally use PRISM to find reachable part of scheduler and export to dot file
prism -importtrans adv.tra -mdp -importstates adv.sta -importlabels adv.lab -exporttrans scheduler_time.tra -exportstates scheduler_time.sta -exporttransrewards scheduler_time.rew -exporttransdotstates scheduler_time.dot -fixdl

# first compute optimal expected energy and export digital clocks MDP
prism scheduler.prism scheduler.props -prop 3 -ptamethod digital -exportdigital digital.prism

# next compute optimal scheduler (from MDP)
prism digital.prism scheduler.props -prop 3 -exportadvmdp adv.tra -exportstates adv.sta -exportlabels adv.lab -exporttransrewards adv.rew

# finally use PRISM to find reachable part of scheduler and export to dot file
prism -importtrans adv.tra -mdp -importstates adv.sta -importlabels adv.lab -exporttrans scheduler_energy.tra -exportstates scheduler_energy.sta -exporttransrewards scheduler_energy.rew -exporttransdotstates scheduler_energy.dot -fixdl

#------------------------------------------------------------------------------
# Version with random execution times
#------------------------------------------------------------------------------

prism scheduler_prob.prism scheduler.props -prop 2 -ptamethod digital -exportdigital digital.prism

prism digital.prism scheduler.props -prop 2 -exportadvmdp adv.tra -exportstates adv.sta -exportlabels adv.lab -exporttransrewards adv.rew

prism -importtrans adv.tra -mdp -importstates adv.sta -importlabels adv.lab -exporttrans scheduler_prob_time.tra -exportstates scheduler_prob_time.sta -exporttransrewards scheduler_prob_time.rew -exporttransdotstates scheduler_prob_time.dot -fixdl

prism scheduler_prob.prism scheduler.props -prop 3 -ptamethod digital -exportdigital digital.prism

prism digital.prism scheduler.props -prop 3 -exportadvmdp adv.tra -exportstates adv.sta -exportlabels adv.lab -exporttransrewards adv.rew

prism -importtrans adv.tra -mdp -importstates adv.sta -importlabels adv.lab -exporttrans scheduler_prob_energy.tra -exportstates scheduler_prob_energy.sta -exporttransrewards scheduler_prob_energy.rew -exporttransdotstates scheduler_prob_energy.dot -fixdl

#------------------------------------------------------------------------------
# Version with a faulty processor (set constant p to the failure probability)
#------------------------------------------------------------------------------

prism scheduler_failure.prism -const p=0.1 scheduler.props -prop 2 -ptamethod digital -exportdigital digital.prism

prism digital.prism scheduler.props -prop 2 -exportadvmdp adv.tra -exportstates adv.sta -exportlabels adv.lab -exporttransrewards adv.rew

prism -importtrans adv.tra -mdp -importstates adv.sta -importlabels adv.lab -exporttrans scheduler_failure_time_01.tra -exportstates scheduler_failure_time_01.sta -exporttransrewards scheduler_failure_time_01.rew -exporttransdotstates scheduler_failure_time_01.dot -fixdl

prism scheduler_failure.prism -const p=0.1 scheduler.props -prop 3 -ptamethod digital -exportdigital digital.prism

prism digital.prism scheduler.props -prop 3 -exportadvmdp adv.tra -exportstates adv.sta -exportlabels adv.lab -exporttransrewards adv.rew

prism -importtrans adv.tra -mdp -importstates adv.sta -importlabels adv.lab -exporttrans scheduler_failure_energy_01.tra -exportstates scheduler_failure_energy_01.sta -exporttransrewards scheduler_failure_energy_01.rew -exporttransdotstates scheduler_failure_energy_01.dot -fixdl