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

module Options
4
    (InputFormat(..),OutputFormat(..),RefinementType(..),RefinementOption(..),
Philipp Meyer's avatar
Philipp Meyer committed
5
     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
26
data RefinementType = TrapRefinement
                    | SiphonRefinement
                    | UTrapRefinement
                    | USiphonRefinement
27
28
                    deriving (Show,Read)

29
30
31
32
data RefinementOption = RefDefault
                      | RefList [RefinementType]
                      | RefAll

Philipp Meyer's avatar
Philipp Meyer committed
33
34
35
36
data Options = Options { inputFormat :: InputFormat
                       , optVerbosity :: Int
                       , optShowHelp :: Bool
                       , optShowVersion :: Bool
Philipp Meyer's avatar
Philipp Meyer committed
37
                       , optProperties :: [Property]
38
                       , optRefinementType :: RefinementOption
39
                       , optMinimizeRefinement :: Int
40
                       , optSMTAuto :: Bool
Philipp Meyer's avatar
Philipp Meyer committed
41
42
43
44
45
46
47
48
                       , optInvariant :: Bool
                       , optOutput :: Maybe String
                       , outputFormat :: OutputFormat
                       , optUseProperties :: Bool
                       , optPrintStructure :: Bool
                       }

startOptions :: Options
49
startOptions = Options { inputFormat = InPP
Philipp Meyer's avatar
Philipp Meyer committed
50
51
52
53
                       , optVerbosity = 1
                       , optShowHelp = False
                       , optShowVersion = False
                       , optProperties = []
54
                       , optRefinementType = RefDefault
55
                       , optMinimizeRefinement = 0
56
                       , optSMTAuto = True
Philipp Meyer's avatar
Philipp Meyer committed
57
58
                       , optInvariant = False
                       , optOutput = Nothing
59
                       , outputFormat = OutDOT
Philipp Meyer's avatar
Philipp Meyer committed
60
61
62
63
                       , optUseProperties = True
                       , optPrintStructure = False
                       }

64
65
66
defaultOptions :: Options
defaultOptions = startOptions{ optProperties = [LayeredTermination, StrongConsensus] }

Philipp Meyer's avatar
Philipp Meyer committed
67
68
options :: [ OptDescr (Options -> Either String Options) ]
options =
Philipp Meyer's avatar
Philipp Meyer committed
69
        [ Option "" ["layered-termination"]
70
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
71
                   optProperties = optProperties opt ++ [LayeredTermination]
72
               }))
Philipp Meyer's avatar
Philipp Meyer committed
73
        "Prove that the protocol satisfies layered termination"
74

Philipp Meyer's avatar
Philipp Meyer committed
75
        , Option "" ["strong-consensus"]
76
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
77
                   optProperties = optProperties opt ++ [StrongConsensus]
78
               }))
Philipp Meyer's avatar
Philipp Meyer committed
79
        "Prove that the protocol satisfies strong consensus"
80

81
82
83
84
        , Option "i" ["invariant"]
        (NoArg (\opt -> Right opt { optInvariant = True }))
        "Generate an invariant"

85
        , Option "r" ["refinement"]
86
87
        (ReqArg (\arg opt ->
                    let addRef ref =
88
89
90
91
                            case optRefinementType opt of
                               RefDefault -> RefList [ref]
                               (RefList refs) -> RefList (refs ++ [ref])
                               RefAll -> RefAll
92
                    in case arg of
93
94
95
96
97
98
                                "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 }
99
                                _ -> Left ("invalid argument for refinement method: " ++ arg)
100
101
                )
                "METHOD")
102
        ("Refine with METHOD (trap, siphon, utrap, usiphon, none, all)")
Philipp Meyer's avatar
Philipp Meyer committed
103

Philipp Meyer's avatar
Philipp Meyer committed
104
105
106
107
108
109
110
111
112
113
        , Option "s" ["structure"]
        (NoArg (\opt -> Right opt { optPrintStructure = True }))
        "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
114
115
116
117
118
        , Option "o" ["output"]
        (ReqArg (\arg opt -> Right opt {
                        optOutput = Just arg
                })
                "FILE")
119
        "Write population protocol to FILE"
Philipp Meyer's avatar
Philipp Meyer committed
120
121
122
123
124

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

125
        , Option "m" ["minimize"]
126
127
128
        (ReqArg (\arg opt -> case reads arg of
                        [(i, "")] -> Right opt { optMinimizeRefinement = i }
                        _ -> Left ("invalid argument for minimization method: " ++ arg)
129
130
                )
                "METHOD")
131
132
        "Minimize size of refinement structure by method METHOD (1-4)"

133
134
135
136
        , Option "" ["smt-disable-auto-config"]
        (NoArg (\opt -> Right opt { optSMTAuto = False }))
        "Disable automatic configuration of the SMT solver"

Philipp Meyer's avatar
Philipp Meyer committed
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
        , 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
158
159
            ([], files, []) ->
                return $ (,files) <$> (return defaultOptions)
Philipp Meyer's avatar
Philipp Meyer committed
160
161
162
163
164
            (actions, files, []) ->
                return $ (,files) <$> foldl (>>=) (return startOptions) actions
            (_, _, errs) -> return $ Left $ concat errs

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