blob: 98ef58161e7c9f2066ff391ae4c454d055765a6a (
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
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
|
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]
, 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]
}
repairConfig :: !*DTMC -> *(!RepairConfig, !*DTMC)
|
