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.