| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Command.Standalone
Description
Transform a specification into a standalone Copilot specification.
Synopsis
- command :: CommandOptions -> IO (Result ErrorCode)
- commandLogic :: Maybe String -> Maybe FilePath -> String -> [(String, String)] -> ExprPairT a -> Spec a -> ExceptT ErrorTriplet IO AppData
- data AppData
- data CommandOptions = CommandOptions {
- commandConditionExpr :: Maybe String
- commandInputFile :: Maybe FilePath
- commandTargetDir :: FilePath
- commandTemplateDir :: Maybe FilePath
- commandFormat :: String
- commandPropFormat :: String
- commandTypeMapping :: [(String, String)]
- commandFilename :: String
- commandPropVia :: Maybe String
- commandExtraVars :: Maybe FilePath
- type ErrorCode = Int
Documentation
Arguments
| :: CommandOptions | Customization options |
| -> IO (Result ErrorCode) |
Generate a new standalone Copilot monitor that implements the spec in an input file.
PRE: The file given is readable, contains a valid file with recognizable
format, the formulas in the file do not use any identifiers that exist in
Copilot, or any of prop, clock, ftp, notPreviousNot. All identifiers
used are valid C99 identifiers. The template, if provided, exists and uses
the variables needed by the standalone application generator. The target
directory is writable and there's enough disk space to copy the files over.
commandLogic :: Maybe String -> Maybe FilePath -> String -> [(String, String)] -> ExprPairT a -> Spec a -> ExceptT ErrorTriplet IO AppData Source #
Generate the data of a new standalone Copilot monitor that implements the spec, using a subexpression handler.
Data that may be relevant to generate a ROS application.
Instances
data CommandOptions Source #
Options used to customize the conversion of specifications to Copilot code.
Constructors
| CommandOptions | |
Fields
| |