Main.hs 18.2 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 Data.Maybe
9
import qualified Data.ByteString.Lazy as L
Philipp Meyer's avatar
Philipp Meyer committed
10
import Control.Monad.Reader
Philipp Meyer's avatar
Philipp Meyer committed
11

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

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

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

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

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

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

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

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

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

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

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

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

289
290
291
getLivenessInvariant :: PetriNet -> Formula Transition -> [Cut] -> OptIO (Maybe [LivenessInvariant])
getLivenessInvariant net f cuts = do
        simp <- opt optSimpFormula
292
        dnfCuts <- generateCuts net f cuts
293
294
        verbosePut 2 $ "Number of " ++ (if simp > 0 then "simplified " else "") ++
                       "disjuncts: " ++ show (length dnfCuts)
295
296
297
298
299
        --
        --z <- conciliate (transitions net)
        --    (checkSimpleCuts dnfCuts) (transitionVectorConstraints net)
        --verbosePut 0 $ "Conciliated set: " ++ show z
        --
300
        rs <- mapM (checkSat . checkLivenessInvariantSat net) dnfCuts
301
302
303
        let added = map (Just . cutToLivenessInvariant) cuts
        return $ sequence (rs ++ added)

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

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

Philipp Meyer's avatar
Philipp Meyer committed
339
340
findLivenessRefinementBySComponent :: PetriNet -> FiringVector ->
        OptIO (Maybe Cut)
341
findLivenessRefinementBySComponent net x =
342
343
344
345
346
        checkSatMin $ checkSComponentSat net x

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

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

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

Philipp Meyer's avatar
Philipp Meyer committed
380
381
checkStructuralProperty :: PetriNet -> Structure -> OptIO PropResult
checkStructuralProperty net struct =
382
383
384
385
        if checkStructure net struct then
            return Satisfied
        else
            return Unsatisfied
386

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

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

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

422
423
424
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
425
        exitWith $ ExitFailure 3