fsml

A library for describing and describing synchronous finite state machines
IN THIS PACKAGE
Module Fsml . Parse
exception Error of int * int * string * string

Raised when parsing PPX nodes

val guard : string -> Guard.t

guard s builds an guard from a string representation. The syntax of the string is exp, where exp denotes a boolean expression.

For example : start='1' or k<2

Raises Error if parsing s or if exp does not denote a boolean expression.

The Parse.guard function can be invoked using the %fsm_guard PPX extension. In this case, Parse.guard s is denoted [%fsm_guard s]

When using the PPX extension, syntax errors in the transition description are detected and reported at compile time.

val guards : string -> Guard.t list

guard s builds a list of guards from a string representation. The syntax of the string is exp1,...,expn, where each expi denotes a boolean expression.

For example : start='1', k<2

Raises Error if parsing s or if expi does not denote a boolean expression.

The Parse.guards function can be invoked using the %fsm_guards PPX extension. In this case, Parse.guards s is denoted [%fsm_guards s]

When using the PPX extension, syntax errors in the transition description are detected and reported at compile time.

val action : string -> Action.t

action s builds an action from a string representation. The syntax of the string is var := exp

For example : rdy:=0

Raises Error if parsing s fails.

The Parse.action function can be invoked using the %fsm_action PPX extension. In this case, Parse.action s is denoted [%fsm_action s]

When using the PPX extension, syntax errors in the transition description are detected and reported at compile time.

val actions : string -> Action.t list

action s builds a list of actions from a string representation. The syntax of the string is act1, ..., actn where act is an action.

For example : rdy:=0, s:=1

Raises Error if parsing s fails.

The Parse.actions function can be invoked using the %fsm_actions PPX extension. In this case, Parse.actions s is denoted [%fsm_actions s]

When using the PPX extension, syntax errors in the transition description are detected and reported at compile time.

val transition : string -> Transition.t

transition s builds a transition from a string representation. The syntax of the string is

src -> dst [ when guard1 , ... , guardm ] [ with act1 , ... , actn ]

where

  • src is the name of the source state
  • dst is the name of the destination state
  • guard is a boolean expression
  • act is an action, of the form var := exp

For example : t = Parse.transition "S0 -> S1 when s=0 with rdy:=0, k:=k=1"

Raises Error if parsing s fails.

The Parse.transition function can be invoked using the %fsm_trans PPX extension. In this case, Parse.transition s is denoted [%fsm_trans s].

When using the PPX extension, syntax errors in the transition description are detected and reported at compile time.

val fsm : string -> Fsm.t

fsm s builds a FSM from a string representation. The syntax of the string is

"name: name ;

states: state1, ..., statens ;

inputs: in1, ..., inni ;

outputs: out1, ..., outno ;

[vars: var1, ..., varnv ;]

trans: t1; ...; tnt ;

itrans: -> state [with act1, ..., actna]"

where

  • name is the name of defined FSM
  • state1, ..., statens is a comma-separated list of state names
  • in1, ..., inni is a comma-separated list of input names
  • out1, ..., outno is a comma-separated list of output names
  • var1, ..., outnv is an optional, comma-separated list of local variable names
  • t1, ..., tnt is a semicolon-separated list of transitions (with syntax defined in transition)
  • act1, ..., actna is an optional, comma-separated list of initial actions

For example : "name: f1; states: E0, E1; inputs: e; outputs: s; trans: E0 -> E1 when e=1 with s:=1; E1 -> E0 when e=0 with s:=0; itrans: -> Init with s:=0;"

Raises Error if parsing s fails.

The Parse.fsm function can be invoked using the %fsm PPX extension. In this case, Parse.fsm s is denoted [%fsm s].

When using the PPX extension, syntax errors in the transition description are detected and reported at compile time.

val stimuli : string -> Tevents.t list

stimuli s builds a sequence of stimuli from a string representation. The syntax of the string is

"name : t1 , v1 ; ..., ; tm , vm"

where t is a clock cycle counter and v a value.

For example, the sequence stimuli "start: 0,'1'; 2,'0'", where start is a signal of type bool

  • set start to '1' (true) at time step 0
  • set start to '0' (false) at time step 2

The Parse.stimuli function can be invoked using the %fsm_stim PPX extension. In this case, Parse.stimuli s is denoted [%fsm_stim s].

Raises Error if parsing s fails.

When using the PPX extension, syntax errors in the transition description are detected and reported at compile time.