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

# Compute optimal expected time; export digital clocks MDP
prism scheduler.nm scheduler.pctl -prop 2 -ptamethod digital -exportdigital digital.nm

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

# 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

# -------------------------------------------------------------------------------------

# Compute optimal expected energy; export digital clocks MDP
prism scheduler.nm scheduler.pctl -prop 3 -ptamethod digital -exportdigital digital.nm

# Compute optimal scheduler (from MDP)
prism digital.nm scheduler.pctl -prop 3 -exportadvmdp adv.tra -exportstates adv.sta -exportlabels adv.lab -exporttransrewards adv.rew

# 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
# -------------------------------------------------------------------------------------

# Compute optimal expected time; export digital clocks MDP
prism scheduler_prob2.nm scheduler.pctl -prop 2 -ptamethod digital -exportdigital digital.nm

# Compute optimal scheduler (from MDP)
prism digital.nm scheduler.pctl -prop 2 -exportadvmdp adv.tra -exportstates adv.sta -exportlabels adv.lab -exporttransrewards adv.rew

# 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_prob_time.tra -exportstates scheduler_prob_time.sta -exporttransrewards scheduler_prob_time.rew -exporttransdotstates scheduler_prob_time.dot -fixdl

# -------------------------------------------------------------------------------------

# Compute optimal expected energy; export digital clocks MDP
prism scheduler_prob2.nm scheduler.pctl -prop 3 -ptamethod digital -exportdigital digital.nm

# Compute optimal scheduler (from MDP)
prism digital.nm scheduler.pctl -prop 3 -exportadvmdp adv.tra -exportstates adv.sta -exportlabels adv.lab -exporttransrewards adv.rew

# 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_prob_energy.tra -exportstates scheduler_prob_energy.sta -exporttransrewards scheduler_prob_energy.rew -exporttransdotstates scheduler_prob_energy.dot -fixdl

# -------------------------------------------------------------------------------------
# Version with a faulty processor
# -------------------------------------------------------------------------------------

# Compute optimal expected time; export digital clocks MDP
prism scheduler_failure.nm -const p=0.1 scheduler.pctl -prop 2 -ptamethod digital -exportdigital digital.nm

# Compute optimal scheduler (from MDP)
prism digital.nm scheduler.pctl -prop 2 -exportadvmdp adv.tra -exportstates adv.sta -exportlabels adv.lab -exporttransrewards adv.rew

# 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_failure_time_01.tra -exportstates scheduler_failure_time_01.sta -exporttransrewards scheduler_failure_time_01.rew -exporttransdotstates scheduler_failure_time_01.dot -fixdl

# -------------------------------------------------------------------------------------

# Compute optimal expected energy; export digital clocks MDP
prism scheduler_failure.nm -const p=0.1 scheduler.pctl -prop 3 -ptamethod digital -exportdigital digital.nm

# Compute optimal scheduler (from MDP)
prism digital.nm scheduler.pctl -prop 3 -exportadvmdp adv.tra -exportstates adv.sta -exportlabels adv.lab -exporttransrewards adv.rew

# 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_failure_energy_01.tra -exportstates scheduler_failure_energy_01.sta -exporttransrewards scheduler_failure_energy_01.rew -exporttransdotstates scheduler_failure_energy_01.dot -fixdl