Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Command.Standalone
Description
Transform a specification into a standalone Copilot specification.
Synopsis
- command :: CommandOptions -> IO (Result ErrorCode)
- commandLogic :: FilePath -> String -> [(String, String)] -> ExprPairT a -> Spec a -> ExceptT ErrorTriplet IO AppData
- data AppData
- data CommandOptions = CommandOptions {}
- 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 :: 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
ToJSON AppData Source # | |
Generic AppData Source # | |
type Rep AppData Source # | |
Defined in Command.Standalone type Rep AppData = D1 ('MetaData "AppData" "Command.Standalone" "ogma-core-1.7.0-AqVFSyaTJa9Cu7bViQd6so" 'False) (C1 ('MetaCons "AppData" 'PrefixI 'True) ((S1 ('MetaSel ('Just "externs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Just "internals") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :*: (S1 ('MetaSel ('Just "reqs") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: (S1 ('MetaSel ('Just "triggers") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Just "specName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))))) |
data CommandOptions Source #
Options used to customize the conversion of specifications to Copilot code.
Constructors
CommandOptions | |
Fields
|