Statechart :: s_cevents : Events /* all events */ s_scbvars : Bvars /* all bvars */ s_cnames : Paths /* min. path suffixes */ s_scstate : State /* Rootstate */ Statenames = Statename -set Statename = Str Paths = Pathname -set Path = Str * Bvars = Bvar -set Bvar = Str States = State -set State = AND-State | OR-State | Basic-State AND-State :: s_aname : Statename s_asubstates : States OR-State :: s_oname : Statename s_osubstates : States s_odefaults : Statenames s_otrs : Trs s_oconns : Connectors BASIC-States :: s_bname : Statename Connectors = Connector -set Connector = s_cname : Conname Conname = Str Trs = Tr -set Tr :: s_tsource : TrAnchor s_ttarget : TrAnchor s_tlabel : Label Label :: s_tguard : Guard s_taction : Action TrAnchor = Statename | Conname | UNDEFINED Guard = s_emptyexpr : Dummy | s_event : Event | s_bvar : Bvar | s_negguard : Guard | s_compp : Comppath | s_compg : Compguard | s_undet : Str Comppath :: s_pop : Pathop s_ppath : Path Pathop :: IN | ENTERED | EXITED Compguard :: s_eop : Op s_elhs : Guard s_erhs : Guard Op = ANDOP | OROP | IMPLIES | EQUIV Action = s_block : Aseq | s_egen : Event | s_bstmt : Boolstmt | s_empty : Dummy Aseq = Action * Boolstmt = s_mtrue : Bvar | s_mfalse : Bvar | s_bass : Bassign Bassign :: s_blhs : Bvar s_brhs : Cond Dummy = Str