LivenessInvariant.hs 847 Bytes
Newer Older
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
module Solver.LivenessInvariant (
    checkLivenessInvariant
  , checkLivenessInvariantSat
  , getLivenessInvariant
  , PlaceVector
  , LivenessInvariant
) where

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

checkLivenessInvariant :: PetriNet -> [String] -> ModelI -> ModelSI -> SBool
checkLivenessInvariant net fired ax m =
        checkPrePostPlaces net m &&&
        checkPrePostTransitions net m &&&
        checkSubsetTransitions fired m &&&
        checkNotEmpty fired m &&&
        checkClosed net ax m &&&
        checkTokens net m &&&
        checkBinary m

checkLivenessInvariantSat :: PetriNet -> [String] -> ModelI ->
        ([String], ModelSI -> SBool)
checkLivenessInvariantSat net fired ax =

getLivenessInvariant :: PetriNet -> ModelI -> ModelI -> LivenessInvariant
getLivenessInvariant net ax as =