A Markov decision process (MDP) reachability probability generation tool for NUS CS4211 Formal Methods for Software Engineering course project: Applying Probabilistic Model Checking in Tennis Match Analytics.
GenPred <input> <output>input: A directory containing several.pcspfiles.output: A file in.csvformat.
GenPred will verify all PCSP models in the input directory by calling the dynamic link libraries (DLLs) of Process Analysis Toolkit (PAT) and store the minimal and maximal reachability probabilities of winning states to output, which will then be evaluated by the betting simulator.