The name of the initial branch for new projects is now "main" instead of "master". Existing projects remain unchanged. More information: https://doku.lrz.de/display/PUBLIC/GitLab

Main.hs 18 KB
Newer Older
1 2
module Main where

3
import System.Exit
4 5
import System.IO
import Control.Monad
6
import Control.Concurrent.ParallelIO
7
import Control.Arrow (first)
Philipp Meyer's avatar
Philipp Meyer committed
8
import Data.List (partition)
9
import Data.Maybe
10
import qualified Data.ByteString.Lazy as L
Philipp Meyer's avatar
Philipp Meyer committed
11
import Control.Monad.Reader
Philipp Meyer's avatar
Philipp Meyer committed
12

Philipp Meyer's avatar
Philipp Meyer committed
13
import Util
Philipp Meyer's avatar
Philipp Meyer committed
14
import Options
15 16
import Parser
import qualified Parser.PNET as PNET
Philipp Meyer's avatar
Philipp Meyer committed
17
import qualified Parser.LOLA as LOLA
18
import qualified Parser.TPN as TPN
19
import qualified Parser.MIST as MIST
20
import PetriNet
21
import Printer
22 23
import qualified Printer.LOLA as LOLAPrinter
import qualified Printer.SARA as SARAPrinter
Philipp Meyer's avatar
Philipp Meyer committed
24
import qualified Printer.SPEC as SPECPrinter
25
import qualified Printer.DOT as DOTPrinter
26
import Property
27
import Structure
28
import Solver
29
import Solver.StateEquation
Philipp Meyer's avatar
Philipp Meyer committed
30
import Solver.TrapConstraints
31
import Solver.TransitionInvariant
32
import Solver.SubnetEmptyTrap
33
import Solver.LivenessInvariant
34
import Solver.SafetyInvariant
35
import Solver.SComponentWithCut
36
import Solver.SComponent
37
import Solver.Simplifier
38
--import Solver.Interpolant
39
--import Solver.CommFreeReachability
40

Philipp Meyer's avatar
Philipp Meyer committed
41 42 43 44
writeFiles :: String -> PetriNet -> [Property] -> OptIO ()
writeFiles basename net props = do
        format <- opt outputFormat
        verbosePut 1 $ "Writing " ++ showNetName net ++ " to " ++
45 46 47
                                  basename ++ " in format " ++ show format
        case format of
            OutLOLA -> do
Philipp Meyer's avatar
Philipp Meyer committed
48
                liftIO $ L.writeFile basename $ LOLAPrinter.printNet net
49 50
                mapM_ (\(p,i) -> do
                        let file = basename ++ ".task" ++ show i
Philipp Meyer's avatar
Philipp Meyer committed
51
                        verbosePut 1 $ "Writing " ++ showPropertyName p
52
                                                 ++ " to " ++ file
Philipp Meyer's avatar
Philipp Meyer committed
53
                        liftIO $ L.writeFile file $ LOLAPrinter.printProperty p
54 55
                      ) (zip props [(1::Integer)..])
            OutSARA -> do
Philipp Meyer's avatar
Philipp Meyer committed
56 57
                liftIO $ L.writeFile basename $ LOLAPrinter.printNet net
                verbosePut 1 $ "Writing properties to " ++ basename ++
58
                                         ".sara"
Philipp Meyer's avatar
Philipp Meyer committed
59
                liftIO $ L.writeFile (basename ++ ".sara") $
60 61 62 63
                    SARAPrinter.printProperties basename net props
            OutSPEC ->
                mapM_ (\(p,i) -> do
                        let file = basename ++ ".target" ++ show i
Philipp Meyer's avatar
Philipp Meyer committed
64
                        verbosePut 1 $ "Writing " ++ showPropertyName p
65
                                                 ++ " to " ++ file
Philipp Meyer's avatar
Philipp Meyer committed
66
                        liftIO $ L.writeFile file $ SPECPrinter.printProperty p
67 68
                      ) (zip props [(1::Integer)..])
            OutDOT ->
Philipp Meyer's avatar
Philipp Meyer committed
69
                liftIO $ L.writeFile basename $ DOTPrinter.printNet net
70

Philipp Meyer's avatar
Philipp Meyer committed
71
structuralAnalysis :: PetriNet -> OptIO ()
72 73 74 75 76 77 78 79 80 81 82 83
structuralAnalysis net =  do
        let noGhost t = t `notElem` ghostTransitions net
        let initP  = filter (\x -> (not . any noGhost . pre net) x &&
                             (any noGhost . post net) x) (places net)
        let finalP = filter (\x -> (not . any noGhost . post net) x &&
                             (any noGhost . pre net) x) (places net)
        let isolP  = filter (\x -> (not . any noGhost . post net) x &&
                             (not . any noGhost . pre net) x) (places net)
        let initT  = filter (\t -> noGhost t && null (pre  net t))
                        (transitions net)
        let finalT = filter (\t -> noGhost t && null (post net t))
                        (transitions net)
Philipp Meyer's avatar
Philipp Meyer committed
84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102
        verbosePut 0 $ "Places             : " ++ show (length (places net))
        verbosePut 0 $ "Transitions        : " ++ show (length (transitions net))
        verbosePut 0 $ "Initial places     : " ++ show (length initP)
        verbosePut 0 $ "Initial transitions: " ++ show (length initT)
        verbosePut 0 $ "Isolated places    : " ++ show (length isolP)
        verbosePut 0 $ "Final places       : " ++ show (length finalP)
        verbosePut 0 $ "Final transitions  : " ++ show (length finalT)

checkFile :: String -> OptIO PropResult
checkFile file = do
        verbosePut 0 $ "Reading \"" ++ file ++ "\""
        format <- opt inputFormat
        let parser = case format of
                             PNET -> PNET.parseContent
                             LOLA -> LOLA.parseContent
                             TPN -> TPN.parseContent
                             MIST -> MIST.parseContent
        (net,props) <- liftIO $ parseFile parser file
        useProperties <- opt optUseProperties
103
        let props' = if useProperties then props else []
Philipp Meyer's avatar
Philipp Meyer committed
104
        implicitProperties <- opt optProperties
105
        let props'' = props' ++ map (makeImplicitProperty net) implicitProperties
Philipp Meyer's avatar
Philipp Meyer committed
106
        transformations <- opt optTransformations
107
        let (net',props''') = foldl transformNet (net,props'') transformations
Philipp Meyer's avatar
Philipp Meyer committed
108 109
        verbosePut 1 $ "Analyzing " ++ showNetName net
        verbosePut 2 $
110 111
                "Places: " ++ show (length  $ places net') ++ "; " ++
                "Transitions: " ++ show (length $ transitions net')
Philipp Meyer's avatar
Philipp Meyer committed
112
        printStruct <- opt optPrintStructure
113
        when printStruct $ structuralAnalysis net
Philipp Meyer's avatar
Philipp Meyer committed
114 115
        verbosePut 3 $ show net'
        output <- opt optOutput
116
        case output of
117
            Just outputfile ->
Philipp Meyer's avatar
Philipp Meyer committed
118
                writeFiles outputfile net' props'''
119
            Nothing -> return ()
Philipp Meyer's avatar
Philipp Meyer committed
120
        -- TODO: short-circuit?
Philipp Meyer's avatar
Philipp Meyer committed
121 122
        rs <- mapM (checkProperty net') props'''
        verbosePut 0 ""
123
        return $ resultsAnd rs
124

125 126
placeOp :: Op -> (Place, Integer) -> Formula Place
placeOp op (p,w) = LinearInequation (Var p) op (Const w)
127

128 129
transformNet :: (PetriNet, [Property]) -> NetTransformation ->
               (PetriNet, [Property])
130
transformNet (net, props) TerminationByReachability =
131 132 133 134 135 136 137 138 139
        let m1 = Place "'m1"
            m2 = Place "'m1"
            sigma = Place "'sigma"
            switch = Transition "'switch"
            primePlace = renamePlace prime
            primeTransition = renameTransition prime
            ps = [sigma, m1, m2] ++
                 places net ++ map primePlace (places net)
            is = [(Place "'m1", 1)] ++
140
                 linitials net ++ map (first primePlace) (linitials net)
141 142
            transformTransition t =
                let (preT, postT) = context net t
143 144 145 146
                    pre'  = [(m1,1)] ++ preT  ++ map (first primePlace) preT
                    post' = [(m1,1)] ++ postT ++ map (first primePlace) postT
                    pre''  = (m2,1) : map (first primePlace) preT
                    post'' = [(m2,1), (sigma,1)] ++ map (first primePlace) postT
147
                in  if t `elem` ghostTransitions net then
148
                        [(t, (pre', post'))]
149
                    else
150 151
                        [(t, (pre', post')), (primeTransition t, (pre'', post''))]
            ts = (switch, ([(m1,1)], [(m2,1)])) :
152 153
                 concatMap transformTransition (transitions net)
            gs = ghostTransitions net
154
            prop = Property "termination by reachability" $ Safety $
155 156 157
                    foldl (:&:) (LinearInequation (Var sigma) Ge (Const 1))
                      (map (\p -> LinearInequation
                                (Var (primePlace p) :-: Var p) Ge (Const 0))
158
                        (places net))
159
            -- TODO: map existing liveness properties
Philipp Meyer's avatar
Philipp Meyer committed
160
        in  (makePetriNetWithTrans (name net) ps ts is gs, prop : props)
161
transformNet (net, props) ValidateIdentifiers =
162 163
        (renamePetriNetPlacesAndTransitions validateId net,
         map (renameProperty validateId) props)
164

165
makeImplicitProperty :: PetriNet -> ImplicitProperty -> Property
166
makeImplicitProperty net Termination =
167
        Property "termination" $ Liveness $
168
            foldl (:&:) FTrue
169
                (map (\t -> LinearInequation (Var t) Eq (Const 0))
170
                    (ghostTransitions net))
171
makeImplicitProperty net ProperTermination =
Philipp Meyer's avatar
Philipp Meyer committed
172
        let (finals, nonfinals) = partition (null . lpost net) (places net)
173
        in  Property "proper termination" $ Safety
Philipp Meyer's avatar
Philipp Meyer committed
174 175
            (foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) finals) :&:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals))
176
makeImplicitProperty net DeadlockFree =
177
        Property "deadlock-free" $ Safety $
178 179
            foldl (:&:) FTrue
                (map (foldl (:|:) FFalse . map (placeOp Lt) . lpre net)
180
                     (filter (`notElem` ghostTransitions net) (transitions net)))
181
makeImplicitProperty net DeadlockFreeUnlessFinal =
182
        let (Property _ (Safety pf)) = makeImplicitProperty net DeadlockFree
183
            (finals, nonfinals) = partition (null . lpost net) (places net)
184
        in  Property "deadlock-free unless final" $ Safety $
Philipp Meyer's avatar
Philipp Meyer committed
185 186
            (foldl (:&:) FTrue  (map (\p -> placeOp Eq (p,0)) finals) :|:
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals)) :&:
187
            pf
188 189 190 191 192
makeImplicitProperty net FinalStateUnreachable =
        let (finals, nonfinals) = partition (null . lpost net) (places net)
        in  Property "final state unreachable" $ Safety $
             foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) finals) :&:
             foldl (:&:) FTrue (map (\p -> placeOp Eq (p,0)) nonfinals)
193
makeImplicitProperty net (Bounded k) =
194
        Property (show k ++ "-bounded") $ Safety $
195
            foldl (:|:) FFalse
Philipp Meyer's avatar
Philipp Meyer committed
196
                (map (\p -> placeOp Ge (p,k+1))
197 198
                    (filter (`notElem` concatMap (post net) (ghostTransitions net))
                        (places net)))
199 200
makeImplicitProperty net Safe =
        let bounded = makeImplicitProperty net (Bounded 1)
201 202 203
        in  Property "safe" $ pcont bounded
makeImplicitProperty _ StructFreeChoice =
        Property "free choice" $ Structural FreeChoice
204 205 206 207
makeImplicitProperty _ StructParallel =
        Property "parallel" $ Structural Parallel
makeImplicitProperty _ StructFinalPlace =
        Property "final place" $ Structural FinalPlace
208 209
makeImplicitProperty _ StructCommunicationFree =
        Property "communication free" $ Structural CommunicationFree
210

Philipp Meyer's avatar
Philipp Meyer committed
211 212 213 214
checkProperty :: PetriNet -> Property -> OptIO PropResult
checkProperty net p = do
        verbosePut 1 $ "\nChecking " ++ showPropertyName p
        verbosePut 3 $ show p
215
        r <- case pcont p of
Philipp Meyer's avatar
Philipp Meyer committed
216 217 218 219
            (Safety pf) -> checkSafetyProperty net pf
            (Liveness pf) -> checkLivenessProperty net pf
            (Structural ps) -> checkStructuralProperty net ps
        verbosePut 0 $ showPropertyName p ++ " " ++
220 221 222 223
            case r of
                Satisfied -> "is satisfied."
                Unsatisfied -> "is not satisfied."
                Unknown-> "may not be satisfied."
224 225
        return r

Philipp Meyer's avatar
Philipp Meyer committed
226 227 228 229
checkSafetyProperty :: PetriNet ->
        Formula Place -> OptIO PropResult
checkSafetyProperty net f = do
        r <- checkSafetyProperty' net f []
230
        case r of
Philipp Meyer's avatar
Philipp Meyer committed
231 232
            (Nothing, traps) -> do
                invariant <- opt optInvariant
233
                if invariant then do
Philipp Meyer's avatar
Philipp Meyer committed
234 235
                    r' <- checkSat $ checkSafetyInvariantSat net f traps
                    printInvariant r'
236 237 238 239 240
                else
                    return Satisfied
            (Just _, _) ->
                return Unknown

Philipp Meyer's avatar
Philipp Meyer committed
241 242
printInvariant :: (Show a) => Maybe [a] -> OptIO PropResult
printInvariant invResult =
Philipp Meyer's avatar
Philipp Meyer committed
243 244
        case invResult of
            Nothing -> do
Philipp Meyer's avatar
Philipp Meyer committed
245
                verbosePut 0 "No invariant found"
Philipp Meyer's avatar
Philipp Meyer committed
246 247
                return Unknown
            Just inv -> do
Philipp Meyer's avatar
Philipp Meyer committed
248 249
                verbosePut 0 "Invariant found"
                mapM_ (putLine . show) inv
Philipp Meyer's avatar
Philipp Meyer committed
250 251
                return Satisfied

Philipp Meyer's avatar
Philipp Meyer committed
252 253 254 255
checkSafetyProperty' :: PetriNet ->
        Formula Place -> [Trap] -> OptIO (Maybe Marking, [Trap])
checkSafetyProperty' net f traps = do
        r <- checkSat $ checkStateEquationSat net f traps
256
        case r of
257
            Nothing -> return (Nothing, traps)
Philipp Meyer's avatar
Philipp Meyer committed
258
            Just m -> do
259 260
                refine <- opt optRefinementType
                if isJust refine then
Philipp Meyer's avatar
Philipp Meyer committed
261
                    refineSafetyProperty net f traps m
262
                else
263
                    return (Just m, traps)
Philipp Meyer's avatar
Philipp Meyer committed
264

Philipp Meyer's avatar
Philipp Meyer committed
265 266 267 268
refineSafetyProperty :: PetriNet ->
        Formula Place -> [Trap] -> Marking -> OptIO (Maybe Marking, [Trap])
refineSafetyProperty net f traps m = do
        r <- checkSat $ checkTrapSat net m
269
        case r of
Philipp Meyer's avatar
Philipp Meyer committed
270 271 272
            Nothing ->
                return (Just m, traps)
            Just trap ->
Philipp Meyer's avatar
Philipp Meyer committed
273
                checkSafetyProperty' net f (trap:traps)
274

Philipp Meyer's avatar
Philipp Meyer committed
275 276 277
checkLivenessProperty :: PetriNet ->
        Formula Transition -> OptIO PropResult
checkLivenessProperty net f = do
278 279
        (r, cuts) <- checkLivenessProperty' net f []
        verbosePut 2 $ "Number of refinements: " ++ show (length cuts)
280
        case r of
281
            Nothing -> do
Philipp Meyer's avatar
Philipp Meyer committed
282
                invariant <- opt optInvariant
283 284
                if invariant then
                    getLivenessInvariant net f cuts >>= printInvariant
285 286
                else
                    return Satisfied
287
            Just _ ->
288
                return Unknown
289

290 291
getLivenessInvariant :: PetriNet -> Formula Transition -> [Cut] -> OptIO (Maybe [LivenessInvariant])
getLivenessInvariant net f cuts = do
292
        dnfCuts <- generateCuts net f cuts
293
        verbosePut 2 $ "Number of disjuncts: " ++ show (length dnfCuts)
294
        rs <- mapM (checkSat . checkLivenessInvariantSat net) dnfCuts
295 296 297
        let added = map (Just . cutToLivenessInvariant) cuts
        return $ sequence (rs ++ added)

Philipp Meyer's avatar
Philipp Meyer committed
298 299 300 301
checkLivenessProperty' :: PetriNet ->
        Formula Transition -> [Cut] -> OptIO (Maybe FiringVector, [Cut])
checkLivenessProperty' net f cuts = do
        r <- checkSat $ checkTransitionInvariantSat net f cuts
Philipp Meyer's avatar
Philipp Meyer committed
302
        case r of
303
            Nothing -> return (Nothing, cuts)
Philipp Meyer's avatar
Philipp Meyer committed
304
            Just x -> do
305 306 307 308 309 310
                rt <- findLivenessRefinement net x
                case rt of
                    Nothing ->
                        return (Just x, cuts)
                    Just cut ->
                        checkLivenessProperty' net f (cut:cuts)
311

Philipp Meyer's avatar
Philipp Meyer committed
312 313 314
findLivenessRefinement :: PetriNet -> FiringVector ->
        OptIO (Maybe Cut)
findLivenessRefinement net x = do
315 316
        refinementType <- opt optRefinementType
        case refinementType of
317
            Just TrapRefinement ->
318
                findLivenessRefinementByEmptyTraps net (initialMarking net) x []
319
            Just SComponentRefinement -> do
320 321 322 323 324
                r1 <- findLivenessRefinementBySComponent net x
                case r1 of
                    Nothing -> findLivenessRefinementByEmptyTraps net
                                                      (initialMarking net) x []
                    Just _ -> return r1
325 326 327 328 329 330 331
            Just SComponentWithCutRefinement -> do
                r1 <- findLivenessRefinementBySComponentWithCut net x
                case r1 of
                    Nothing -> findLivenessRefinementByEmptyTraps net
                                                      (initialMarking net) x []
                    Just _ -> return r1
            Nothing -> return Nothing
332

Philipp Meyer's avatar
Philipp Meyer committed
333 334
findLivenessRefinementBySComponent :: PetriNet -> FiringVector ->
        OptIO (Maybe Cut)
335
findLivenessRefinementBySComponent net x =
336 337 338 339 340
        checkSatMin $ checkSComponentSat net x

findLivenessRefinementBySComponentWithCut :: PetriNet -> FiringVector ->
        OptIO (Maybe Cut)
findLivenessRefinementBySComponentWithCut net x =
341
        checkSatMin $ checkSComponentWithCutSat net x
342

Philipp Meyer's avatar
Philipp Meyer committed
343 344 345
findLivenessRefinementByEmptyTraps :: PetriNet -> Marking -> FiringVector ->
        [Trap] -> OptIO (Maybe Cut)
findLivenessRefinementByEmptyTraps net m x traps = do
346
        r <- checkSatMin $ checkSubnetEmptyTrapSat net m x
347 348
        case r of
            Nothing -> do
Philipp Meyer's avatar
Philipp Meyer committed
349
                rm <- refineSafetyProperty net FTrue traps m
350
                case rm of
351
                    (Nothing, _) -> do
352
                        cut <- generateLivenessRefinement net x traps
353
                        return $ Just cut
354 355 356
                    (Just _, _) ->
                        return Nothing
            Just trap -> do
357
                let traps' = trap:traps
358
                rm <- local (\opts -> opts { optRefinementType = Nothing }) $
Philipp Meyer's avatar
Philipp Meyer committed
359
                            checkSafetyProperty' net FTrue traps'
360
                case rm of
361
                    (Nothing, _) -> do
362
                        cut <- generateLivenessRefinement net x traps'
363
                        return $ Just cut
364
                    (Just m', _) ->
Philipp Meyer's avatar
Philipp Meyer committed
365
                        findLivenessRefinementByEmptyTraps net m' x traps'
366

367 368
generateLivenessRefinement :: PetriNet -> FiringVector -> [Trap] -> OptIO Cut
generateLivenessRefinement net x traps = do
369
        -- TODO: also use better cuts for traps
370
        let cut = constructCut net x traps
Philipp Meyer's avatar
Philipp Meyer committed
371
        verbosePut 3 $ "- cut: " ++ show cut
372
        return cut
373

Philipp Meyer's avatar
Philipp Meyer committed
374 375
checkStructuralProperty :: PetriNet -> Structure -> OptIO PropResult
checkStructuralProperty net struct =
376 377 378 379
        if checkStructure net struct then
            return Satisfied
        else
            return Unsatisfied
380

381
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
382
main = do
383
        putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
384 385 386 387 388
        args <- parseArgs
        case args of
            Left err -> exitErrorWith err
            Right (opts, files) -> do
                when (optShowVersion opts) (exitSuccessWith "Version 0.01")
Philipp Meyer's avatar
Philipp Meyer committed
389
                when (optShowHelp opts) (exitSuccessWith usageInformation)
390
                when (null files) (exitErrorWith "No input file given")
Philipp Meyer's avatar
Philipp Meyer committed
391 392 393 394 395
                let opts' = opts {
                        optProperties = reverse (optProperties opts),
                        optTransformations= reverse (optTransformations opts)
                    }
                rs <- runReaderT (mapM checkFile files) opts'
Philipp Meyer's avatar
Philipp Meyer committed
396
                -- TODO: short-circuit with Control.Monad.Loops?
397 398 399 400 401 402 403
                case resultsAnd rs of
                    Satisfied ->
                        exitSuccessWith "All properties satisfied."
                    Unsatisfied ->
                        exitFailureWith "Some properties are not satisfied"
                    Unknown ->
                        exitFailureWith "Some properties may not be satisfied."
404

Philipp Meyer's avatar
Philipp Meyer committed
405
-- TODO: Always exit with exit code 0 unless an error occured
406 407 408
exitSuccessWith :: String -> IO ()
exitSuccessWith msg = do
        putStrLn msg
409
        cleanupAndExitWith ExitSuccess
410 411 412 413

exitFailureWith :: String -> IO ()
exitFailureWith msg = do
        putStrLn msg
414
        cleanupAndExitWith $ ExitFailure 2
Philipp Meyer's avatar
Philipp Meyer committed
415

416 417 418
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
419 420 421 422 423 424
        cleanupAndExitWith $ ExitFailure 3

cleanupAndExitWith :: ExitCode -> IO ()
cleanupAndExitWith code = do
        stopGlobalPool
        exitWith code