summaryrefslogtreecommitdiff
path: root/Assignment2/src/DTMC.dcl
blob: 5b491ae438fa35fcde26c9d016cedff372ca5836 (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
definition module DTMC

from Data.Map import :: Map
from Data.Maybe import :: Maybe
from System.FilePath import :: FilePath

:: *DTMC =
	{ nr_states :: !Int
	, states    :: !*{Maybe State}
	}

:: State =
	{ state_id    :: !Int
	, transitions :: !Map Int String
	, init        :: !Bool
	}

// Note that state_id must be an absorbing state
// (Probability, state_id)
:: Property :== (Real, Int)

stateElimination :: !*DTMC -> *DTMC
parseDTMC :: !FilePath !*World -> *(!*DTMC, !*World)
printDTMC :: !*DTMC -> *(!String, !*DTMC)
addVars :: *DTMC -> *DTMC