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.SComponent
35
import Solver.Simplifier
36
--import Solver.Interpolant
37
--import Solver.CommFreeReachability
38

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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