ogma-core-1.14.0: Ogma: Helper tool to interoperate between Copilot and other languages.

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.