StateMachine → SysML v2 State Definition Generation

Since StateMachine is type-parametric, concrete string representations are provided externally via StateMachineRepr.

structure VerifiedMBSE.Output.TransitionRepr : Type

TransitionRepr: string representation of a transition.

• name : String
• sourceName : String
• targetName : String
• guardDesc : String
• effectDesc : String

structure VerifiedMBSE.Output.StateRepr : Type

StateRepr: string representation of a state.

• name : String
• doc : String

structure VerifiedMBSE.Output.StateMachineRepr : Type

StateMachineRepr: string representation of a state machine.

• name : String
• states : List StateRepr
• initialState : String
• transitions : List TransitionRepr

def VerifiedMBSE.Output.stateToSysML (s : StateRepr) (lvl : ℕ) : String

Generate state definitions.

Equations

• One or more equations did not get rendered due to their size.

def VerifiedMBSE.Output.transitionToSysML (t : TransitionRepr) (lvl : ℕ) : String

Generate transition definitions.

Equations

• One or more equations did not get rendered due to their size.

def VerifiedMBSE.Output.stateMachineToSysML (repr : StateMachineRepr) (lvl : ℕ) : String

StateMachineRepr → SysML v2 state def。

Equations

• One or more equations did not get rendered due to their size.

def VerifiedMBSE.Output.StateMachineRepr.toSysML (repr : StateMachineRepr) : String

StateMachineRepr.toSysML: top-level generation.

Equations

• repr.toSysML = VerifiedMBSE.Output.stateMachineToSysML repr 0