package lascar

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

Finite State Machines

A FSM is a LTS

  • with an added set of local variables
  • for which state attributes may include output valuations
  • for which transition labels are pairs of conditions and actions on inputs, outputs and local variables.
module type T = sig ... end
module Make (S : Ltsa.STATE) (V : Fsm_value.T) : T with type state = S.t and module Value = V and type Valuation.value = V.t and type Transition.Condition.Expr.value = V.t and type Transition.Action.Expr.value = V.t
module Trans (S1 : T) (S2 : T) : sig ... end

Functor for converting a FSM, with a given implementation of state identifiers and values into another one with different respective implementations