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

3
import System.Exit
4
5
import System.IO
import Control.Monad
6
import Control.Concurrent.ParallelIO
7
import Control.Arrow (first)
8
import Data.List (partition,minimumBy,genericLength)
9
import Data.Ord (comparing)
10
import Data.Maybe
11
import qualified Data.ByteString.Lazy as L
Philipp Meyer's avatar
Philipp Meyer committed
12
import Control.Monad.Reader
Philipp Meyer's avatar
Philipp Meyer committed
13

Philipp Meyer's avatar
Philipp Meyer committed
14
import Util
Philipp Meyer's avatar
Philipp Meyer committed
15
import Options
16
import Parser
17
18
import qualified Parser.PP as PPParser
import PopulationProtocol
19
import Printer
20
import qualified Printer.DOT as DOTPrinter
21
import Property
22
import StructuralComputation
23
import Solver
24
import Solver.TerminalMarkingsUniqueConsensus
25
import Solver.TerminalMarkingReachable
26

27
28
writeFiles :: String -> PopulationProtocol -> [Property] -> OptIO ()
writeFiles basename pp props = do
Philipp Meyer's avatar
Philipp Meyer committed
29
        format <- opt outputFormat
30
        verbosePut 1 $ "Writing " ++ showNetName pp ++ " to " ++
31
32
33
                                  basename ++ " in format " ++ show format
        case format of
            OutDOT ->
34
                liftIO $ L.writeFile basename $ DOTPrinter.printPopulationProtocol pp
35

36
37
38
39
40
41
42
structuralAnalysis :: PopulationProtocol -> OptIO ()
structuralAnalysis pp =  do
        verbosePut 0 $ "States             : " ++ show (length (states pp))
        verbosePut 0 $ "Transitions        : " ++ show (length (transitions pp))
        verbosePut 0 $ "Initial states     : " ++ show (length (initialStates pp))
        verbosePut 0 $ "Yes states         : " ++ show (length (yesStates pp))
        verbosePut 0 $ "No states          : " ++ show (length (noStates pp))
Philipp Meyer's avatar
Philipp Meyer committed
43
44
45
46
47
48

checkFile :: String -> OptIO PropResult
checkFile file = do
        verbosePut 0 $ "Reading \"" ++ file ++ "\""
        format <- opt inputFormat
        let parser = case format of
49
50
                             InPP -> PPParser.parseContent
        (pp,props) <- liftIO $ parseFile parser file
Philipp Meyer's avatar
Philipp Meyer committed
51
        implicitProperties <- opt optProperties
52
53
        let props' = props ++ map (makeImplicitProperty pp) implicitProperties
        verbosePut 1 $ "Analyzing " ++ showNetName pp
Philipp Meyer's avatar
Philipp Meyer committed
54
        verbosePut 2 $
55
                "Number of states: " ++ show (length (states pp))
56
        verbosePut 2 $
57
58
59
                "Number of transitions: " ++ show (length (transitions pp))
        let pRowSize p = let (preP, postP) = context pp p in length preP + length postP
        let arcs = sum $ map pRowSize $ states pp
60
61
        verbosePut 2 $
                "Number of arcs: " ++ show arcs
Philipp Meyer's avatar
Philipp Meyer committed
62
        printStruct <- opt optPrintStructure
63
64
        when printStruct $ structuralAnalysis pp
        verbosePut 3 $ show pp
Philipp Meyer's avatar
Philipp Meyer committed
65
        output <- opt optOutput
66
        case output of
67
            Just outputfile ->
68
                writeFiles outputfile pp props'
69
            Nothing -> return ()
70
        -- TODO: short-circuit? parallel?
71
        rs <- mapM (checkProperty pp) props'
Philipp Meyer's avatar
Philipp Meyer committed
72
        verbosePut 0 ""
73
        return $ resultsAnd rs
74

75

76
makeImplicitProperty :: PopulationProtocol -> ImplicitProperty -> Property
77
makeImplicitProperty _ TerminalMarkingsUniqueConsensus =
78
        Property "reachable terminal markings have a unique consensus" $ Constraint TerminalMarkingsUniqueConsensusConstraint
79
80
makeImplicitProperty _ TerminalMarkingReachable =
        Property "terminal marking reachable" $ Constraint TerminalMarkingReachableConstraint
81

82
83
checkProperty :: PopulationProtocol -> Property -> OptIO PropResult
checkProperty pp p = do
Philipp Meyer's avatar
Philipp Meyer committed
84
85
        verbosePut 1 $ "\nChecking " ++ showPropertyName p
        verbosePut 3 $ show p
86
        r <- case pcont p of
87
88
89
--            (Safety pf) -> checkSafetyProperty pp pf
--            (Liveness pf) -> checkLivenessProperty pp pf
            (Constraint pc) -> checkConstraintProperty pp pc
Philipp Meyer's avatar
Philipp Meyer committed
90
        verbosePut 0 $ showPropertyName p ++ " " ++
91
92
93
94
            case r of
                Satisfied -> "is satisfied."
                Unsatisfied -> "is not satisfied."
                Unknown-> "may not be satisfied."
95
96
        return r

97
98
99
printInvariant :: (Show a, Invariant a) => (Maybe [a], [a]) -> OptIO PropResult
printInvariant (baseInvResult, addedInv) =
        case baseInvResult of
Philipp Meyer's avatar
Philipp Meyer committed
100
            Nothing -> do
Philipp Meyer's avatar
Philipp Meyer committed
101
                verbosePut 0 "No invariant found"
Philipp Meyer's avatar
Philipp Meyer committed
102
                return Unknown
103
            Just baseInv -> do
Philipp Meyer's avatar
Philipp Meyer committed
104
                verbosePut 0 "Invariant found"
105
106
107
                let baseSize = map invariantSize baseInv
                let addedSize = map invariantSize addedInv
                verbosePut 2 $ "Number of atoms in base invariants: " ++ show baseSize ++
108
                        " (total of " ++ show (sum baseSize) ++ ")"
109
                verbosePut 2 $ "Number of atoms in added invariants: " ++ show addedSize ++
110
                        " (total of " ++ show (sum addedSize) ++ ")"
111
112
                mapM_ (putLine . show) baseInv
                mapM_ (putLine . show) addedInv
Philipp Meyer's avatar
Philipp Meyer committed
113
114
                return Satisfied

115
116
checkConstraintProperty :: PopulationProtocol -> ConstraintProperty -> OptIO PropResult
checkConstraintProperty pp cp =
117
        case cp of
118
119
            TerminalMarkingsUniqueConsensusConstraint -> checkTerminalMarkingsUniqueConsensusProperty pp
            TerminalMarkingReachableConstraint -> checkTerminalMarkingReachableProperty pp
120

121
122
123
checkTerminalMarkingsUniqueConsensusProperty :: PopulationProtocol -> OptIO PropResult
checkTerminalMarkingsUniqueConsensusProperty pp = do
        r <- checkTerminalMarkingsUniqueConsensusProperty' pp [] [] []
124
        case r of
125
126
            (Nothing, _, _, _) -> return Satisfied
            (Just _, _, _, _) -> return Unknown
127

128
checkTerminalMarkingsUniqueConsensusProperty' :: PopulationProtocol ->
129
130
        [Trap] -> [Siphon] -> [StableInequality] ->
        OptIO (Maybe TerminalMarkingsUniqueConsensusCounterExample, [Trap], [Siphon], [StableInequality])
131
132
checkTerminalMarkingsUniqueConsensusProperty' pp utraps usiphons inequalities = do
        r <- checkSat $ checkTerminalMarkingsUniqueConsensusSat pp utraps usiphons inequalities
133
        case r of
134
            Nothing -> return (Nothing, utraps, usiphons, inequalities)
135
            Just c -> do
136
137
                refine <- opt optRefinementType
                if isJust refine then
138
                    refineTerminalMarkingsUniqueConsensusProperty pp utraps usiphons inequalities c
139
                else
140
                    return (Just c, utraps, usiphons, inequalities)
141

142
refineTerminalMarkingsUniqueConsensusProperty :: PopulationProtocol ->
143
144
        [Trap] -> [Siphon] -> [StableInequality] -> TerminalMarkingsUniqueConsensusCounterExample ->
        OptIO (Maybe TerminalMarkingsUniqueConsensusCounterExample, [Trap], [Siphon], [StableInequality])
145
146
refineTerminalMarkingsUniqueConsensusProperty pp utraps usiphons inequalities c@(m0, m1, m2, x1, x2) = do
        r1 <- checkSatMin $ Solver.TerminalMarkingsUniqueConsensus.findTrapConstraintsSat pp m0 m1 m2 x1 x2
147
148
        case r1 of
            Nothing -> do
149
                r2 <- checkSatMin $ Solver.TerminalMarkingsUniqueConsensus.findUSiphonConstraintsSat pp m0 m1 m2 x1 x2
150
151
                case r2 of
                    Nothing -> do
152
                        r3 <- checkSatMin $ Solver.TerminalMarkingsUniqueConsensus.findUTrapConstraintsSat pp m0 m1 m2 x1 x2
Philipp J. Meyer's avatar
Philipp J. Meyer committed
153
                        case r3 of
154
                            Nothing -> return (Just c, utraps, usiphons, inequalities)
Philipp J. Meyer's avatar
Philipp J. Meyer committed
155
                            Just utrap ->
156
                                checkTerminalMarkingsUniqueConsensusProperty' pp (utrap:utraps) usiphons inequalities
Philipp J. Meyer's avatar
Philipp J. Meyer committed
157
                    Just usiphon ->
158
                        checkTerminalMarkingsUniqueConsensusProperty' pp utraps (usiphon:usiphons) inequalities
159
            Just trap ->
160
                checkTerminalMarkingsUniqueConsensusProperty' pp (trap:utraps) usiphons inequalities
161

162
163
164
165
checkTerminalMarkingReachableProperty :: PopulationProtocol -> OptIO PropResult
checkTerminalMarkingReachableProperty pp = do
        let nonTrivialTriplets = filter (not . trivialTriplet) $ generateTriplets pp
        checkTerminalMarkingReachableProperty' pp nonTrivialTriplets 1 $ genericLength $ transitions pp
166

167
168
checkTerminalMarkingReachableProperty' :: PopulationProtocol -> [Triplet] -> Integer -> Integer -> OptIO PropResult
checkTerminalMarkingReachableProperty' pp triplets k kmax = do
169
        verbosePut 1 $ "Checking terminal marking reachable with at most " ++ show k ++ " partitions"
170
        r <- checkSatMin $ checkTerminalMarkingReachableSat pp triplets k
171
        case r of
172
173
            Nothing ->
                if k < kmax then
174
                    checkTerminalMarkingReachableProperty' pp triplets (k + 1) kmax
175
176
                else
                    return Unknown
177
178
179
180
181
182
183
            Just inv -> do
                invariant <- opt optInvariant
                if invariant then
                    printInvariant (Just inv, [])
                else
                    return Satisfied

184
main :: IO ()
Philipp Meyer's avatar
Philipp Meyer committed
185
main = do
Philipp Meyer's avatar
Philipp Meyer committed
186
        putStrLn "Peregrine - Efficient Verification of Population Protocols\n"
187
188
189
190
191
        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
192
                when (optShowHelp opts) (exitSuccessWith usageInformation)
193
                when (null files) (exitErrorWith "No input file given")
194
                let opts' = opts { optProperties = reverse (optProperties opts) }
Philipp Meyer's avatar
Philipp Meyer committed
195
                rs <- runReaderT (mapM checkFile files) opts'
196
197
                -- TODO: short-circuit with Control.Monad.Loops? parallel
                -- execution?
198
199
200
201
202
203
204
                case resultsAnd rs of
                    Satisfied ->
                        exitSuccessWith "All properties satisfied."
                    Unsatisfied ->
                        exitFailureWith "Some properties are not satisfied"
                    Unknown ->
                        exitFailureWith "Some properties may not be satisfied."
205

Philipp Meyer's avatar
Philipp Meyer committed
206
-- TODO: Always exit with exit code 0 unless an error occured
207
208
209
exitSuccessWith :: String -> IO ()
exitSuccessWith msg = do
        putStrLn msg
210
        cleanupAndExitWith ExitSuccess
211
212
213
214

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

217
218
219
exitErrorWith :: String -> IO ()
exitErrorWith msg = do
        hPutStrLn stderr msg
220
221
222
223
224
225
        cleanupAndExitWith $ ExitFailure 3

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