Main.hs 18.1 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
12
import qualified Data.Set as S
Philipp Meyer's avatar
Philipp Meyer committed
13

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

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

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

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

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

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

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

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

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

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

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

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

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

Philipp Meyer's avatar
Philipp Meyer committed
299
300
301
302
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
303
        case r of
304
            Nothing -> return (Nothing, cuts)
Philipp Meyer's avatar
Philipp Meyer committed
305
            Just x -> do
306
307
308
309
310
311
                rt <- findLivenessRefinement net x
                case rt of
                    Nothing ->
                        return (Just x, cuts)
                    Just cut ->
                        checkLivenessProperty' net f (cut:cuts)
312

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

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

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

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

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

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

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

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

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

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

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