LivenessInvariant.hs 2.79 KB
Newer Older
1
2
3
4
5
6
7
8
module Solver.LivenessInvariant (
    checkLivenessInvariant
  , checkLivenessInvariantSat
  , getLivenessInvariant
  , PlaceVector
  , LivenessInvariant
) where

9
10
11
12
13
14
15
import Data.SBV

import Solver
import Solver.SComponent
import PetriNet

type PlaceVector = [(String, Integer)]
16
17
type LivenessInvariant = [PlaceVector]

18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
type Cut = ([String], Bool)
type NamedCut = (String, [(String, Cut)])

nameCuts :: [[Cut]] -> [NamedCut]
nameCuts cuts =
            map (\(n, c) -> (n, numPref "@comp" `zip` c)) $
                numPref "@cut" `zip` cuts
        where
            numPref s = map (\i -> s ++ show i) [(1::Integer)..]

varNames :: PetriNet -> [NamedCut] -> [String]
varNames net = concatMap cutNames
        where
            cutNames (n, c) =
                [n ++ "@comp0"] ++
                map (\p -> n ++ "@p" ++ p) (places net) ++
                map (\(n', _) -> n ++ n') c

foldComps :: [SCompCut] -> [[Cut]]
foldComps = foldl combine [[]]
        where
            combine cuts (t1, t2, u) =
                concatMap
                    (\c -> [(t1, True) : c, (t2, True) : c, (u, False) : c]) cuts

checkCut :: PetriNet -> ModelSI -> NamedCut -> SBool
checkCut net m (n, comps) =
            bAnd (map checkTransition (transitions net)) &&&
            mVal m (n ++ "@comp0") + sum (map addComp2 comps) .> 0 &&&
            bAnd (map (\p -> checkNonNegativity (n ++ "@p" ++ p)) (places net)) &&&
            checkNonNegativity (n ++ "@comp0") &&&
            bAnd (map (\(n', _) -> checkNonNegativity (n ++ n')) comps)
        where checkTransition t =
                let incoming = map addPlace $ lpre net t
                    outgoing = map addPlace $ lpost net t
                    zeroComp = mVal m (n ++ "@comp0")
                    addComp1 (n', (ts, xv)) =
                        if t `elem` ts then
                            (if xv then 1 else (-1)) * mVal m (n ++ n')
                        else
                            0
                    cutComps = map addComp1 comps
                in  sum outgoing - sum incoming + zeroComp .<= sum cutComps
              addPlace (p,w) = literal w * mVal m (n ++ "@p" ++ p)
              addComp2 (n', (_, w)) = if w then 0 else mVal m (n ++ n')
              checkNonNegativity x = mVal m x .>= 0

checkLivenessInvariant :: PetriNet -> [NamedCut] ->
        ModelSI -> SBool
checkLivenessInvariant net cuts m =
        bAnd (map (checkCut net m) cuts)

checkLivenessInvariantSat :: PetriNet -> [SCompCut] ->
71
        ([String], ModelSI -> SBool)
72
73
74
75
76
checkLivenessInvariantSat net comps =
        let cuts = foldComps comps
            namedCuts = nameCuts cuts
            names = varNames net namedCuts
        in  (names, checkLivenessInvariant net namedCuts)
77

78
79
getLivenessInvariant :: PetriNet -> [SCompCut] -> ModelI -> LivenessInvariant
getLivenessInvariant net ax as = undefined