definition module DTMC

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

from StdOverloaded import class toString

:: *DTMC =
	{ nr_states  :: !Int
	, parameters :: ![String]
	, unzero     :: ![String]
	, states     :: !*{Maybe State}
	}

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

:: Op = LT | EQ | GT
instance toString Op

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

:: Properties :== [Property]

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

:: RepairConfig =
	{ totality_restrictions   :: ![String]
	, transition_restrictions :: ![String]
	, minimalisation_goal     :: !String
	}

:: CostFunction
	= SumSquaredErrors
	| NumberModifiedTransitions

repairConfig :: !CostFunction !*DTMC -> *(!RepairConfig, !*DTMC)