Main.hs 17.7 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.SComponentWithCut
34
import Solver.Simplifier
35
import Solver.Interpolant
36
--import Solver.CommFreeReachability
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
getLivenessInvariant :: PetriNet -> Formula Transition -> [Cut] -> OptIO (Maybe [LivenessInvariant])
getLivenessInvariant net f cuts = do
        simp <- opt optSimpFormula
290
        dnfCuts <- generateCuts net f cuts
291
292
        verbosePut 2 $ "Number of " ++ (if simp > 0 then "simplified " else "") ++
                       "disjuncts: " ++ show (length dnfCuts)
293
294
295
296
297
        --
        --z <- conciliate (transitions net)
        --    (checkSimpleCuts dnfCuts) (transitionVectorConstraints net)
        --verbosePut 0 $ "Conciliated set: " ++ show z
        --
298
        rs <- mapM (checkSat . checkLivenessInvariantSat net) dnfCuts
299
300
301
        let added = map (Just . cutToLivenessInvariant) cuts
        return $ sequence (rs ++ added)

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

Philipp Meyer's avatar
Philipp Meyer committed
320
321
322
findLivenessRefinement :: PetriNet -> FiringVector ->
        OptIO (Maybe Cut)
findLivenessRefinement net x = do
323
324
325
326
327
328
329
330
331
332
        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
333

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

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

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

Philipp Meyer's avatar
Philipp Meyer committed
370
371
checkStructuralProperty :: PetriNet -> Structure -> OptIO PropResult
checkStructuralProperty net struct =
372
373
374
375
        if checkStructure net struct then
            return Satisfied
        else
            return Unsatisfied
376

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

Philipp Meyer's avatar
Philipp Meyer committed
401
-- TODO: Always exit with exit code 0 unless an error occured
402
403
404
405
406
407
408
409
exitSuccessWith :: String -> IO ()
exitSuccessWith msg = do
        putStrLn msg
        exitSuccess

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

412
413
414
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
415
        exitWith $ ExitFailure 3