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

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

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

37

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

Philipp Meyer's avatar
Philipp Meyer committed
68
structuralAnalysis :: PetriNet -> OptIO ()
69
70
71
72
73
74
75
76
77
78
79
80
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
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
        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
100
        let props' = if useProperties then props else []
Philipp Meyer's avatar
Philipp Meyer committed
101
        implicitProperties <- opt optProperties
102
        let props'' = props' ++ map (makeImplicitProperty net) implicitProperties
Philipp Meyer's avatar
Philipp Meyer committed
103
        transformations <- opt optTransformations
104
        let (net',props''') = foldl transformNet (net,props'') transformations
Philipp Meyer's avatar
Philipp Meyer committed
105
106
        verbosePut 1 $ "Analyzing " ++ showNetName net
        verbosePut 2 $
107
108
                "Places: " ++ show (length  $ places net') ++ "; " ++
                "Transitions: " ++ show (length $ transitions net')
Philipp Meyer's avatar
Philipp Meyer committed
109
        printStruct <- opt optPrintStructure
110
        when printStruct $ structuralAnalysis net
Philipp Meyer's avatar
Philipp Meyer committed
111
112
        verbosePut 3 $ show net'
        output <- opt optOutput
113
        case output of
114
            Just outputfile ->
Philipp Meyer's avatar
Philipp Meyer committed
115
                writeFiles outputfile net' props'''
116
            Nothing -> return ()
Philipp Meyer's avatar
Philipp Meyer committed
117
        -- TODO: short-circuit?
Philipp Meyer's avatar
Philipp Meyer committed
118
119
        rs <- mapM (checkProperty net') props'''
        verbosePut 0 ""
120
        return $ resultsAnd rs
121

122
123
placeOp :: Op -> (Place, Integer) -> Formula Place
placeOp op (p,w) = LinearInequation (Var p) op (Const w)
124

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

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

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

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

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

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

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

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

287
288
289
290
291
getLivenessInvariant :: PetriNet -> Formula Transition -> [Cut] -> OptIO (Maybe [LivenessInvariant])
getLivenessInvariant net f cuts = do
        simp <- opt optSimpFormula
        let dnfCuts = generateCuts f cuts
        verbosePut 2 $ "Number of disjuncts: " ++ show (length dnfCuts)
292
--        let simpCuts = if simp then simplifyCuts dnfCuts else dnfCuts
293
        let simpCuts = if simp then simplifyCuts dnfCuts else dnfCuts
294
295
296
297
        verbosePut 2 $ "Number of simplified disjuncts (1): " ++ show (length simpCuts)
        simpCuts' <- if simp then simplifyBySubsumption net [] simpCuts else return simpCuts
        verbosePut 2 $ "Number of simplified disjuncts (2): " ++ show (length simpCuts')
        rs <- mapM (checkSat . checkLivenessInvariantSat net) simpCuts'
298
299
300
        let added = map (Just . cutToLivenessInvariant) cuts
        return $ sequence (rs ++ added)

301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
simplifyBySubsumption :: PetriNet -> [SimpleCut] -> [SimpleCut] -> OptIO [SimpleCut]
simplifyBySubsumption _ acc [] = return $ reverse acc
simplifyBySubsumption net acc (c0:cs) = do
        r <- checkSat $ checkSubsumptionSat net c0 (acc ++ cs)
        let acc' = case r of
                    Nothing -> acc
                    Just _ -> c0:acc
        simplifyBySubsumption net acc' cs

removeWith :: (a -> a -> Bool) -> [a] -> [a]
removeWith f = removeCuts' []
        where
            removeCuts' acc [] = reverse acc
            removeCuts' acc (x:xs) = removeCuts' (x : cutFilter x acc) (cutFilter x xs)
            cutFilter cut = filter (not . f cut)

Philipp Meyer's avatar
Philipp Meyer committed
317
318
319
320
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
321
        case r of
322
            Nothing -> return (Nothing, cuts)
Philipp Meyer's avatar
Philipp Meyer committed
323
324
            Just x -> do
                refine <- opt optRefine
325
                if refine then do
Philipp Meyer's avatar
Philipp Meyer committed
326
                    rt <- findLivenessRefinement net x
327
                    case rt of
Philipp Meyer's avatar
Philipp Meyer committed
328
                        Nothing ->
329
                            return (Just x, cuts)
Philipp Meyer's avatar
Philipp Meyer committed
330
                        Just cut ->
Philipp Meyer's avatar
Philipp Meyer committed
331
                            checkLivenessProperty' net f (cut:cuts)
332
                else
333
                    return (Just x, cuts)
334

Philipp Meyer's avatar
Philipp Meyer committed
335
336
337
findLivenessRefinement :: PetriNet -> FiringVector ->
        OptIO (Maybe Cut)
findLivenessRefinement net x = do
338
339
340
341
342
343
344
345
346
347
        refinementType <- opt optRefinementType
        case refinementType of
            TrapRefinement ->
                findLivenessRefinementByEmptyTraps net (initialMarking net) x []
            SComponentRefinement -> do
                r1 <- findLivenessRefinementBySComponent net x
                case r1 of
                    Nothing -> findLivenessRefinementByEmptyTraps net
                                                      (initialMarking net) x []
                    Just _ -> return r1
348

Philipp Meyer's avatar
Philipp Meyer committed
349
350
351
findLivenessRefinementBySComponent :: PetriNet -> FiringVector ->
        OptIO (Maybe Cut)
findLivenessRefinementBySComponent net x =
352
        checkSatMin $ checkSComponentSat net x
353

Philipp Meyer's avatar
Philipp Meyer committed
354
355
356
findLivenessRefinementByEmptyTraps :: PetriNet -> Marking -> FiringVector ->
        [Trap] -> OptIO (Maybe Cut)
findLivenessRefinementByEmptyTraps net m x traps = do
357
        r <- checkSatMin $ checkSubnetEmptyTrapSat net m x
358
359
        case r of
            Nothing -> do
Philipp Meyer's avatar
Philipp Meyer committed
360
                rm <- refineSafetyProperty net FTrue traps m
361
                case rm of
362
                    (Nothing, _) -> do
363
                        cut <- generateLivenessRefinement net x traps
364
                        return $ Just cut
365
366
367
                    (Just _, _) ->
                        return Nothing
            Just trap -> do
368
                let traps' = trap:traps
Philipp Meyer's avatar
Philipp Meyer committed
369
370
                rm <- local (\opts -> opts { optRefine = False }) $
                            checkSafetyProperty' net FTrue traps'
371
                case rm of
372
                    (Nothing, _) -> do
373
                        cut <- generateLivenessRefinement net x traps'
374
                        return $ Just cut
375
                    (Just m', _) ->
Philipp Meyer's avatar
Philipp Meyer committed
376
                        findLivenessRefinementByEmptyTraps net m' x traps'
377

378
379
380
generateLivenessRefinement :: PetriNet -> FiringVector -> [Trap] -> OptIO Cut
generateLivenessRefinement net x traps = do
        let cut = constructCut net x traps
Philipp Meyer's avatar
Philipp Meyer committed
381
        verbosePut 3 $ "- cut: " ++ show cut
382
        return cut
383

Philipp Meyer's avatar
Philipp Meyer committed
384
385
checkStructuralProperty :: PetriNet -> Structure -> OptIO PropResult
checkStructuralProperty net struct =
386
387
388
389
        if checkStructure net struct then
            return Satisfied
        else
            return Unsatisfied
390

391
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
392
main = do
393
        putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
394
395
396
397
398
        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
399
                when (optShowHelp opts) (exitSuccessWith usageInformation)
400
                when (null files) (exitErrorWith "No input file given")
Philipp Meyer's avatar
Philipp Meyer committed
401
402
403
404
405
                let opts' = opts {
                        optProperties = reverse (optProperties opts),
                        optTransformations= reverse (optTransformations opts)
                    }
                rs <- runReaderT (mapM checkFile files) opts'
Philipp Meyer's avatar
Philipp Meyer committed
406
                -- TODO: short-circuit with Control.Monad.Loops?
407
408
409
410
411
412
413
                case resultsAnd rs of
                    Satisfied ->
                        exitSuccessWith "All properties satisfied."
                    Unsatisfied ->
                        exitFailureWith "Some properties are not satisfied"
                    Unknown ->
                        exitFailureWith "Some properties may not be satisfied."
414

Philipp Meyer's avatar
Philipp Meyer committed
415
-- TODO: Always exit with exit code 0 unless an error occured
416
417
418
419
420
421
422
423
exitSuccessWith :: String -> IO ()
exitSuccessWith msg = do
        putStrLn msg
        exitSuccess

exitFailureWith :: String -> IO ()
exitFailureWith msg = do
        putStrLn msg
424
        exitWith $ ExitFailure 2
Philipp Meyer's avatar
Philipp Meyer committed
425

426
427
428
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
429
        exitWith $ ExitFailure 3