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