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

module Options
4
    (InputFormat(..),OutputFormat(..),RefinementType(..),
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)

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

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

options :: [ OptDescr (Options -> Either String Options) ]
options =
Philipp Meyer's avatar
Philipp Meyer committed
62
        [ Option "" ["layered-termination"]
63
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
64
                   optProperties = optProperties opt ++ [LayeredTermination]
65
               }))
Philipp Meyer's avatar
Philipp Meyer committed
66
        "Prove that the protocol satisfies layered termination"
67

Philipp Meyer's avatar
Philipp Meyer committed
68
        , Option "" ["strong-consensus"]
69
        (NoArg (\opt -> Right opt {
Philipp Meyer's avatar
Philipp Meyer committed
70
                   optProperties = optProperties opt ++ [StrongConsensus]
71
               }))
Philipp Meyer's avatar
Philipp Meyer committed
72
        "Prove that the protocol satisfies strong consensus"
73

74
75
76
77
        , Option "i" ["invariant"]
        (NoArg (\opt -> Right opt { optInvariant = True }))
        "Generate an invariant"

78
        , Option "r" ["refinement"]
79
80
81
82
83
84
85
86
87
88
89
90
91
92
        (ReqArg (\arg opt ->
                    let addRef ref =
                            Right opt { optRefinementType =
                                    case optRefinementType opt of
                                       Nothing -> Just [ref]
                                       Just(refs) -> Just (refs ++ [ref])

                            }
                    in case arg of
                                "trap" -> addRef TrapRefinement
                                "siphon" -> addRef SiphonRefinement
                                "utrap" -> addRef UTrapRefinement
                                "usiphon" -> addRef USiphonRefinement
                                _ -> Left ("invalid argument for refinement method: " ++ arg)
93
94
                )
                "METHOD")
95
        ("Refine with METHOD (trap, siphon, utrap, usiphon)")
Philipp Meyer's avatar
Philipp Meyer committed
96

Philipp Meyer's avatar
Philipp Meyer committed
97
98
99
100
101
102
103
104
105
106
        , 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
107
108
109
110
111
        , Option "o" ["output"]
        (ReqArg (\arg opt -> Right opt {
                        optOutput = Just arg
                })
                "FILE")
112
        "Write population protocol to FILE"
Philipp Meyer's avatar
Philipp Meyer committed
113
114
115
116
117

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

118
        , Option "m" ["minimize"]
119
120
121
        (ReqArg (\arg opt -> case reads arg of
                        [(i, "")] -> Right opt { optMinimizeRefinement = i }
                        _ -> Left ("invalid argument for minimization method: " ++ arg)
122
123
                )
                "METHOD")
124
125
        "Minimize size of refinement structure by method METHOD (1-4)"

126
127
128
129
        , 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
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
        , 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
156
usageInformation = usageInfo "Peregrine" options