Safe Haskell	None
Language	Haskell2010

Command.Diagram

Description

Transform a state diagram into a Copilot specification.

Synopsis

diagram :: FilePath -> DiagramOptions -> IO (Result ErrorCode)
data DiagramOptions = DiagramOptions {
- diagramTargetDir :: FilePath
- diagramTemplateDir :: Maybe FilePath
- diagramFormat :: DiagramFormat
- diagramPropFormat :: DiagramPropFormat
- diagramFilename :: String
- diagramMode :: DiagramMode
- diagramStateVar :: String
- diagramInputVar :: String
}
data DiagramFormat
- = Mermaid
- | Dot
data DiagramMode
- = CheckState
- | ComputeState
- | CheckMoves
data DiagramPropFormat
- = Lustre
- | Inputs
- | Literal
- | SMV
type ErrorCode = Int

Documentation

diagram Source #

Arguments

:: FilePath	Path to a file containing a diagram
-> DiagramOptions	Customization options
-> IO (Result ErrorCode)

Generate a new Copilot monitor that implements a state machine described in a diagram given as 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 stateMachine, externalState, main, spec, stateMachine1, clock, ftp, notPreviousNot. All identifiers used are valid C99 identifiers. The template, if provided, exists and uses the variables needed by the diagram application generator. The target directory is writable and there's enough disk space to copy the files over.

data DiagramOptions Source #

Options used to customize the conversion of diagrams to Copilot code.

Constructors

DiagramOptions
Fields diagramTargetDir :: FilePath diagramTemplateDir :: Maybe FilePath diagramFormat :: DiagramFormat diagramPropFormat :: DiagramPropFormat diagramFilename :: String diagramMode :: DiagramMode diagramStateVar :: String diagramInputVar :: String

data DiagramFormat Source #

Diagram formats supported.

Constructors

Mermaid
Dot

Instances

Instances details

Show DiagramFormat Source #
Instance details Defined in Data.Diagram.Parser Methods showsPrec :: Int -> DiagramFormat -> ShowS Source # show :: DiagramFormat -> String Source # showList :: [DiagramFormat] -> ShowS Source #
Eq DiagramFormat Source #
Instance details Defined in Data.Diagram.Parser Methods (==) :: DiagramFormat -> DiagramFormat -> Bool Source # (/=) :: DiagramFormat -> DiagramFormat -> Bool Source #

data DiagramMode Source #

Modes of operation.

Constructors

CheckState	Check if given state matches expectation
ComputeState	Compute expected state
CheckMoves	Check if transitioning to a state would be possible.

Instances

Instances details

Show DiagramMode Source #
Instance details Defined in Language.Trans.Diagram2Copilot Methods showsPrec :: Int -> DiagramMode -> ShowS Source # show :: DiagramMode -> String Source # showList :: [DiagramMode] -> ShowS Source #
Eq DiagramMode Source #
Instance details Defined in Language.Trans.Diagram2Copilot Methods (==) :: DiagramMode -> DiagramMode -> Bool Source # (/=) :: DiagramMode -> DiagramMode -> Bool Source #

data DiagramPropFormat Source #

Property formats supported.

Constructors

Lustre
Inputs
Literal
SMV

Instances

Instances details

Show DiagramPropFormat Source #
Instance details Defined in Command.Diagram Methods showsPrec :: Int -> DiagramPropFormat -> ShowS Source # show :: DiagramPropFormat -> String Source # showList :: [DiagramPropFormat] -> ShowS Source #
Eq DiagramPropFormat Source #
Instance details Defined in Command.Diagram Methods (==) :: DiagramPropFormat -> DiagramPropFormat -> Bool Source # (/=) :: DiagramPropFormat -> DiagramPropFormat -> Bool Source #

type ErrorCode = Int Source #

Encoding of reasons why the command can fail.

The error code used is 1 for user error.