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

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

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

36

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

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

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

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

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

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

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

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

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

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

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

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

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

Philipp Meyer's avatar
Philipp Meyer committed
315
316
317
findLivenessRefinement :: PetriNet -> FiringVector ->
        OptIO (Maybe Cut)
findLivenessRefinement net x = do
318
319
320
321
322
323
324
325
326
327
        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
328

Philipp Meyer's avatar
Philipp Meyer committed
329
330
331
findLivenessRefinementBySComponent :: PetriNet -> FiringVector ->
        OptIO (Maybe Cut)
findLivenessRefinementBySComponent net x =
332
        checkSatMin $ checkSComponentSat net x
333

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

Philipp Meyer's avatar
Philipp Meyer committed
358
359
generateLivenessRefinement :: PetriNet -> FiringVector -> [Trap] -> OptIO Cut
generateLivenessRefinement net x traps = do
360
        let cut = constructCut net x traps
Philipp Meyer's avatar
Philipp Meyer committed
361
        verbosePut 3 $ "- cut: " ++ show cut
362
        return cut
363

Philipp Meyer's avatar
Philipp Meyer committed
364
365
checkStructuralProperty :: PetriNet -> Structure -> OptIO PropResult
checkStructuralProperty net struct =
366
367
368
369
        if checkStructure net struct then
            return Satisfied
        else
            return Unsatisfied
370

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

Philipp Meyer's avatar
Philipp Meyer committed
395
-- TODO: Always exit with exit code 0 unless an error occured
396
397
398
399
400
401
402
403
exitSuccessWith :: String -> IO ()
exitSuccessWith msg = do
        putStrLn msg
        exitSuccess

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

406
407
408
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
409
        exitWith $ ExitFailure 3