<> <> <> DIRECTORY Boole, Core; FiniteStateAutomata: CEDAR DEFINITIONS IMPORTS Boole = BEGIN <> <> <> <> <> <> <> ROPE: TYPE = Core.ROPE; Expression: TYPE = Boole.Expression; StateMachine: TYPE = REF StateMachineRec; StateMachineRec: TYPE = RECORD [ states: States _ NIL, outputs: Outputs _ NIL, initialState: State _ NIL]; States: TYPE = LIST OF State; State: TYPE = REF StateRec; StateRec: TYPE = RECORD [ name: ATOM _ NIL, transitions: Transitions _ NIL]; Transitions: TYPE = LIST OF Transition; Transition: TYPE = REF TransitionRec; TransitionRec: TYPE = RECORD [ expr: Expression _ NIL, target: State _ NIL]; Outputs: TYPE = LIST OF OutputRec; OutputRec: TYPE = RECORD [ output: Core.Wire, expr: Expression]; TransitionLiterals: TYPE = LIST OF TransitionLiteral; TransitionLiteral: TYPE = RECORD [ to: ATOM, expr: Expression]; <> CreateError: SIGNAL [msg: ROPE]; NewMachine: PROC [states: LIST OF ATOM] RETURNS [StateMachine]; NewTransition: PROC [fsa: StateMachine, from, to: ATOM, expr: Expression]; NewTransitions: PROC [fsa: StateMachine, from: ATOM, transitions: TransitionLiterals]; FindState: PROC [fsa: StateMachine, state: ATOM] RETURNS [State]; StateSeq: PROC [states: LIST OF ATOM, root: ROPE, count: NAT] RETURNS [newStates: LIST OF ATOM]; Mealy: PROC [fsa: StateMachine, state: ATOM, outputs: LIST OF Core.Wire, transitions: TransitionLiterals]; <> StateMachineCell: PROC [public: Core.Wire, fsa: StateMachine, name: ROPE _ NIL, props: Core.Properties _ NIL, completeCheck: BOOL _ FALSE, assert: Boole.Expression _ Boole.true] RETURNS [cellType: Core.CellType]; <> < all <=> (NOT assert) OR all = true>> < ~(e1 AND e2) <=> assert AND e1 AND e2 = false>> <> <<>> END.