Options.hs 7.23 KB
Newer Older
Philipp Meyer's avatar
Philipp Meyer committed
1
2
3
{-# LANGUAGE TupleSections #-}

module Options
4
    (InputFormat(..),OutputFormat(..),RefinementType(..),RefinementOption(..),BackendSolver(..),
5
     PropertyOption(..),Options(..),startOptions,options,parseArgs,
Philipp Meyer's avatar
Philipp Meyer committed
6
7
8
9
10
11
12
     usageInformation)
where

import Control.Applicative ((<$>))
import System.Console.GetOpt
import System.Environment (getArgs)

Philipp Meyer's avatar
Philipp Meyer committed
13
14
import Property (Property(..))

15
16
data InputFormat = InPP deriving (Read)
data OutputFormat = OutDOT deriving (Read)
Philipp Meyer's avatar
Philipp Meyer committed
17

18
19
instance Show InputFormat where
        show InPP = "PP"
Philipp Meyer's avatar
Philipp Meyer committed
20
21
22
instance Show OutputFormat where
        show OutDOT = "DOT"

23
24
25
data BackendSolver = Z3
                   | CVC4

26
27
28
29
data RefinementType = TrapRefinement
                    | SiphonRefinement
                    | UTrapRefinement
                    | USiphonRefinement
30
31
                    deriving (Show,Read)

32
33
34
data PropertyOption = PropDefault
                      | PropList [Property]

35
36
37
38
data RefinementOption = RefDefault
                      | RefList [RefinementType]
                      | RefAll

Philipp Meyer's avatar
Philipp Meyer committed
39
40
41
42
data Options = Options { inputFormat :: InputFormat
                       , optVerbosity :: Int
                       , optShowHelp :: Bool
                       , optShowVersion :: Bool
43
                       , optSolver :: BackendSolver
44
                       , optProperties :: PropertyOption
45
                       , optRefinementType :: RefinementOption
46
                       , optMinimizeRefinement :: Int
Philipp Meyer's avatar
Philipp Meyer committed
47
48
49
50
51
52
53
54
                       , optInvariant :: Bool
                       , optOutput :: Maybe String
                       , outputFormat :: OutputFormat
                       , optUseProperties :: Bool
                       , optPrintStructure :: Bool
                       }

startOptions :: Options
55
startOptions = Options { inputFormat = InPP
Philipp Meyer's avatar
Philipp Meyer committed
56
57
58
                       , optVerbosity = 1
                       , optShowHelp = False
                       , optShowVersion = False
59
                       , optSolver = Options.Z3
60
                       , optProperties = PropDefault
61
                       , optRefinementType = RefDefault
62
                       , optMinimizeRefinement = 0
Philipp Meyer's avatar
Philipp Meyer committed
63
64
                       , optInvariant = False
                       , optOutput = Nothing
65
                       , outputFormat = OutDOT
Philipp Meyer's avatar
Philipp Meyer committed
66
67
68
69
                       , optUseProperties = True
                       , optPrintStructure = False
                       }

70
71
72
73
74
75
76
77
addProperty :: Property -> Options -> Either String Options
addProperty prop opt =
        Right opt {
           optProperties = case optProperties opt of
                               PropDefault -> PropList [prop]
                               (PropList props) -> PropList (props ++ [prop])
       }

Philipp Meyer's avatar
Philipp Meyer committed
78
79
options :: [ OptDescr (Options -> Either String Options) ]
options =
Philipp Meyer's avatar
Philipp Meyer committed
80
        [ Option "" ["layered-termination"]
81
        (NoArg (addProperty LayeredTermination))
Philipp Meyer's avatar
Philipp Meyer committed
82
        "Prove that the protocol satisfies layered termination"
83

Philipp Meyer's avatar
Philipp Meyer committed
84
        , Option "" ["strong-consensus"]
85
        (NoArg (addProperty StrongConsensus))
Philipp Meyer's avatar
Philipp Meyer committed
86
        "Prove that the protocol satisfies strong consensus"
87

88
        , Option "" ["correctness"]
89
        (NoArg (addProperty StrongConsensusWithCorrectness))
90
91
        "Prove that the protocol correctly satisfies the given predicate"

92
93
94
95
        , Option "" ["terminal-consensus"]
        (NoArg (addProperty ReachableTermConfigInConsensus))
        "Prove that reachable terminal configurations are in consensus"

96
97
98
99
        , Option "i" ["invariant"]
        (NoArg (\opt -> Right opt { optInvariant = True }))
        "Generate an invariant"

100
101
102
103
104
105
106
107
108
109
        , Option "" ["solver"]
        (ReqArg (\arg opt ->
            case arg of
                        "z3" -> Right opt { optSolver = Options.Z3 }
                        "cvc4" -> Right opt { optSolver = Options.CVC4 }
                        _ -> Left ("invalid argument for refinement method: " ++ arg)
                )
                "SOLVER")
        ("Use backend solver SOLVER (z3, cvc4)")

110
        , Option "r" ["refinement"]
111
112
        (ReqArg (\arg opt ->
                    let addRef ref =
113
114
115
116
                            case optRefinementType opt of
                               RefDefault -> RefList [ref]
                               (RefList refs) -> RefList (refs ++ [ref])
                               RefAll -> RefAll
117
                    in case arg of
118
119
120
121
122
123
                                "none" -> Right opt { optRefinementType = RefList [] }
                                "trap" -> Right opt { optRefinementType = addRef TrapRefinement }
                                "siphon" -> Right opt { optRefinementType = addRef SiphonRefinement }
                                "utrap" -> Right opt { optRefinementType = addRef UTrapRefinement }
                                "usiphon" -> Right opt { optRefinementType = addRef USiphonRefinement }
                                "all" -> Right opt { optRefinementType = RefAll }
124
                                _ -> Left ("invalid argument for refinement method: " ++ arg)
125
126
                )
                "METHOD")
127
        ("Refine with METHOD (trap, siphon, utrap, usiphon, none, all)")
Philipp Meyer's avatar
Philipp Meyer committed
128

Philipp Meyer's avatar
Philipp Meyer committed
129
        , Option "s" ["structure"]
130
131
132
133
134
135
        (NoArg (\opt -> Right opt {
                                  optPrintStructure = True,
                                  optProperties = case optProperties opt of
                                                       PropDefault -> PropList []
                                                       (PropList props) -> PropList props
                        }))
Philipp Meyer's avatar
Philipp Meyer committed
136
137
138
139
140
141
142
143
        "Print structural information"


        , Option "" ["in-pp"]
        (NoArg (\opt -> Right opt { inputFormat = InPP }))
        "Use the population protocol input format"


Philipp Meyer's avatar
Philipp Meyer committed
144
145
146
147
148
        , Option "o" ["output"]
        (ReqArg (\arg opt -> Right opt {
                        optOutput = Just arg
                })
                "FILE")
149
        "Write population protocol to FILE"
Philipp Meyer's avatar
Philipp Meyer committed
150
151
152
153
154

        , Option "" ["out-dot"]
        (NoArg (\opt -> Right opt { outputFormat = OutDOT }))
        "Use the dot output format"

155
        , Option "m" ["minimize"]
156
157
158
        (ReqArg (\arg opt -> case reads arg of
                        [(i, "")] -> Right opt { optMinimizeRefinement = i }
                        _ -> Left ("invalid argument for minimization method: " ++ arg)
159
160
                )
                "METHOD")
161
162
        "Minimize size of refinement structure by method METHOD (1-4)"

Philipp Meyer's avatar
Philipp Meyer committed
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
        , Option "v" ["verbose"]
        (NoArg (\opt -> Right opt { optVerbosity = optVerbosity opt + 1 }))
        "Increase verbosity (may be specified more than once)"

        , Option "q" ["quiet"]
        (NoArg (\opt -> Right opt { optVerbosity = optVerbosity opt - 1 }))
        "Decrease verbosity (may be specified more than once)"

        , Option "V" ["version"]
        (NoArg (\opt -> Right opt { optShowVersion = True }))
        "Show version"

        , Option "h" ["help"]
        (NoArg (\opt -> Right opt { optShowHelp = True }))
        "Show help"
        ]

parseArgs :: IO (Either String (Options, [String]))
parseArgs = do
        args <- getArgs
        case getOpt Permute options args of
            (actions, files, []) ->
                return $ (,files) <$> foldl (>>=) (return startOptions) actions
            (_, _, errs) -> return $ Left $ concat errs

usageInformation :: String
Philipp Meyer's avatar
Philipp Meyer committed
189
190
usageInformation =
        usageInfo ("Usage: peregrine [OPTIONS] FILE\n") options