Prism Models
------------
In all models scenario 2 can be recreated by uncommenting the lines ending with //Scenario 2 and commenting the lines ending with //Scenario 1.
These lines are
const int Miss = 900; // Scenario 1
//const int Miss = 900; // Scenario 2
and
NoOfObjs : [0..3] init 3; // Scenario 1
// NoOfObjs : [0..3] init 3; // Scenario 2
uav_dtmc.prism
--------------
Contains the discrete time markov chain model of the scenario, where the transitions are chosen uniform randomly.
uav_mdp.prism
-------------
Contains the markov decision process model of the scenario. The non-determinism will return maximal and minimal results.
uav_rounded_mdp.prism
---------------------
Non-deterministic markov decision process model of the scenario, where all constants have been rounded manually.
Property Files
--------------
uav_mdp.props
-------------
Contains some properties that are of interest to the models.
uav_mdp.bounded.props
---------------------
Contains the time bound properties needed for the graphs.
Results Files
-------------
result_uav_mdp.txt
------------------
Log file from running all properties in uav_mdp.props against the model in Scenario 1 in uav_mdp.prism.
summary_result_uav_mdp.txt
--------------------------
Summary file containing just the most important information about the properties.
(The columns are; Name, Probability, Time to check, RAM needed for matrix)
Graphs
------
uav_deadline1.gra
-----------------
Prism graph file, containing information from running Scenario 1.
uav_deadline1.pdf
-----------------
Graph resulting from running Scenario 1, produced by prism.
uav_deadline2.gra
-----------------
Prism graph file, containing information from running Scenario 2.
uav_deadline2.pdf
-----------------
Graph resulting from running Scenario 2, produced by prism.