Modeling and Simulation

During the three practical assignments you will create a fully operational probabilistic model checker for discrete time Markov chains (DTMC) and (a variant of) the probabilistic computation tree logic (PCTL) as well as continuous time Markov chains (CTMC) and the continuous stochastic logic (CSL) in Java 1.6. For each of the assignments we will provide the basic framework with the intended class structure. Consequently, your task is to implement the respective methods. You can infer the intended behavior of each method from its Java Doc comments. You will find the framework for this assignment (Practical01.tgz) in the course management system. For your convenience we also provide a basic testing environment in terms of JUnit 3 test cases inside the frameworks. Please note that these tests do by far not cover all methods and do not prove correctness of your code and consequently, we may still manually investigate your submissions. Since the test cases depend on JUnit 3 you should add the respective library to your build path. Please also make sure that the folder test containing several test models can be found by your program.