Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/VDM/VDMSL/simulatorSL/ (Wiener Entwicklungsmethode ^©) Datei vom 13.4.2020 mit Größe 29 kB

Impressum simulator1.vdmsl Sprache: VDM

\documentstyle[11pt,vdmsl]{article}

% a4 style
\oddsidemargin -0.4mm \evensidemargin -0.4mm
\topmargin -10.4mm \headheight 5mm \headsep 8mm
\footheight 5mm \footskip 15mm
\textheight 230mm \textwidth 160mm
\parindent0mm

\title{\Large\bf VDM-SL Specifications for a Simulation Tool - Version I\footnote
{This work is supported by grants from Natural Sciences and
Engineering Research Council, Canada and Concordia University Graduate
Fellowships.}}
\normalsize
\author{V. S. Alagar \and D. Muthiayen}
\date{Department of Computer Science\\ Concordia University\\
Montreal, Quebec H3G 1M8, Canada\\
Phone: +1 (514) 848-3022\\
\{alagar,d\_muthi\}@cs.concordia.ca\\~\\
February 1996}

\begin{document}
\pagenumbering{arabic}
\maketitle
\thispagestyle{empty}

\section{Specifications - Version I}

\begin{vdm_al}

module TROM

   exports all

definitions

types

PortType       :: label       : String
                  cardinality : nat
                  portlist    : seq of Port

inv mk_PortType(label, cardinality, portlist) ==

   (cardinality = card elems portlist);

Event          :: label    : String
                  type     : EventType
                  porttype : PortType

inv mk_Event(label, type, porttype) ==

   (((type = <INTERNAL>) and (porttype.label = "NULLPORT")) or
    ((type = <INPUT>) and (porttype.label <> "NULLPORT")) or
    ((type = <OUTPUT>) and (porttype.label <> "NULLPORT")));

State          :: label     : String
                  type      : StateType
                  isinitial : bool
                  substates : set of State

inv mk_State(label, type, isinitial, substates) ==

   (let exists_entry_state : set of State +> bool
        exists_entry_state(substates) ==
           ((exists1 s in set substates & (s.isinitial = true)) and
            (forall s in set substates &
              (((s.type = <SIMPLE>) and (s.substates = { })) or
               ((s.type = <COMPLEX>) and (exists_entry_state(s.substates))))))
    in
   (((type = <SIMPLE>) and (substates = { })) or
    ((type = <COMPLEX>) and (exists_entry_state(substates)))));

Attribute      :: label : String
                  type  : String;

LSLTrait       :: traitlabel   : String
                  traittype    : String
                  elementtypes : seq of String;

AttrFunction   :: stat       : State
                  attributes : set of Attribute;

TransitionSpec :: label         : String
                  sourcestate   : State
                  destinstate   : State
                  triggerevent  : Event
                  portcondition : bool
                  enabcondition : bool
                  postcondition : bool;

TimeConstraint :: label            : String
                  transition       : TransitionSpec
                  constrainedevent : Event
                  timebounds       : ReactionWindow
                  disablingstates  : set of State
                  reactionwindows  : set of ReactionWindow

inv mk_TimeConstraint(label,transition,cevent,tbounds,dstates,rwindows) ==

   (((cevent.type = <INTERNAL>) or (cevent.type = <OUTPUT>)) and
    (forall rw in set rwindows &
       ((rw.uppertimebound - rw.lowertimebound) =
                         (tbounds.uppertimebound - tbounds.lowertimebound))));

EventType      = <INPUT> | <INTERNAL> | <OUTPUT>;

StateType      = <SIMPLE> | <COMPLEX>;

ReactionWindow :: lowertimebound : nat
                  uppertimebound : nat

inv mk_ReactionWindow(lowertimebound, uppertimebound) ==

   (lowertimebound <= uppertimebound);

Port           :: label : String;

PortLink       :: tromporttuple1 : TromPortTuple
                  tromporttuple2 : TromPortTuple

inv mk_PortLink(tromporttuple1, tromporttuple2) ==

   (tromporttuple1.tromlabel <> tromporttuple2.tromlabel);

TromPortTuple  :: tromlabel : String
                  portlabel : String;

SimulationEvent :: eventlabel   : String
                   tromlabel    : String
                   portlabel    : String
                   occurtime    : nat
                   eventhistory : [EventHistory];

EventHistory    :: triggeredtransition : bool
                   tromcurrentstate    : [State]
                   assignmentvector    : [token]
                   reactionshistory    : set of ReactionHistory;

ReactionHistory :: timeconstraint : TimeConstraint
                   reactionwindow : ReactionWindow
                   reaction       : Reaction;

Reaction = <FIRED> | <DISABLED> | <ENABLED>;

LSLTraitDefinition :: label    : String
                      paramets : seq of String;

String         = seq1 of char;

Trom :: label            : String
        tromclass        : String
        porttypes        : set of PortType
        events           : set of Event
        states           : set of State
        attributes       : set of Attribute
        lsltraits        : set of LSLTrait
        attrfunctions    : set of AttrFunction
        transitionspecs  : set of TransitionSpec
        timeconstraints  : set of TimeConstraint
        currentstate     : State
        assignmentvector : token

inv mk_Trom(label,tromclass,porttypes,events,states,attributes,
            lsltraits,attrfunctions,
      transitionspecs,timeconstraints,currentstate,assignmentvector) ==

   (forall pt1, pt2 in set porttypes &
      (pt1.label = pt2.label => pt1 = pt2)) and

   (forall e1, e2 in set events &
      (e1.label = e2.label => e1 = e2)) and

   (forall s1, s2 in set states &
      (s1.label = s2.label => s1 = s2)) and

   (forall a1, a2 in set attributes &
      (a1.label = a2.label => a1 = a2)) and

   (forall tr1, tr2 in set lsltraits &
      (tr1.traittype = tr2.traittype => tr1 = tr2)) and

   (forall af1, af2 in set attrfunctions &
      (af1.stat = af2.stat => af1 = af2)) and

   (forall ts1, ts2 in set transitionspecs &
      (ts1.label = ts2.label => ts1 = ts2)) and

   (forall tc1, tc2 in set timeconstraints &
      (tc1.label = tc2.label => tc1 = tc2)) and

   (forall e in set events &
      (exists pt in set porttypes & (pt = e.porttype))) and

   (exists1 s in set states &
      (s.isinitial = true)) and

   (exists1 s in set states &
      ((currentstate = s) or (substate_of(currentstate, s)))) and

   (forall a in set attributes &
      ((exists1 pt in set porttypes & (pt.label = a.type)) or
       (exists1 tr in set lsltraits & (tr.traittype = a.type)))) and

   (forall tr in set lsltraits &
      (forall el in set elems tr.elementtypes &
         ((exists1 pt in set porttypes & (pt.label = el)) or
          (exists1 tr2 in set lsltraits & (tr2.traittype = el))))) and

   (forall af in set attrfunctions &
      ((exists1 s in set states & ((s = af.stat) or
                                   (substate_of(af.stat, s)))) and
       (forall afa in set af.attributes &
          (exists1 a in set attributes & (a = afa))))) and

   (forall ts in set transitionspecs &
      ((exists1 s in set states & ((s = ts.sourcestate) or
                                   (substate_of(ts.sourcestate, s)))) and
       (exists1 d in set states & ((d = ts.destinstate) or
                                   (substate_of(ts.destinstate, d)))) and
       (exists1 e in set events & (e = ts.triggerevent)))) and

   (forall tc in set timeconstraints &
      ((exists1 ts in set transitionspecs & (ts = tc.transition)) and
       (exists1 e in set events &
         ((e = tc.constrainedevent) and
          ((e.type = <INTERNAL>) or (e.type = <OUTPUT>)))) and
       (forall ds in set tc.disablingstates &
         (exists1 s in set states & ((s = ds) or (substate_of(ds, s)))))));

Subsystem :: label     : String
             includes  : set of Subsystem
             troms     : set of Trom
             portlinks : set of PortLink

inv mk_Subsystem(label, includes, troms, portlinks) ==

   (forall s1, s2 in set includes &
      (s1.label = s2.label => s1 = s2)) and

   (let included_subsystem : String * set of Subsystem +> bool
        included_subsystem(subsystemlabel, subsystems) ==
           (exists1 s in set subsystems &
              ((s.label = subsystemlabel) or
               (included_subsystem(subsystemlabel, s.includes)))) in

   (not included_subsystem(label, includes))) and

   (forall trom1, trom2 in set troms &
      (trom1.label = trom2.label => trom1 = trom2)) and

   (let included_trom : String * set of Subsystem +> bool
        included_trom(tromlabel, subsystems) ==
           (exists1 s in set subsystems &
              ((exists1 trom in set s.troms &
                  (trom.label = tromlabel)) or
               (included_trom(tromlabel, s.includes)))) in

   (forall trom in set troms &
      (not included_trom(trom.label, includes)))) and

   (let linked_trom : TromPortTuple * set of Trom +> bool
        linked_trom(tptuple, troms) ==
           (exists1 trom in set troms &
              ((trom.label = tptuple.tromlabel) and
               (exists1 pt in set trom.porttypes &
                  (exists1 p in set elems pt.portlist &
                     (p.label = tptuple.portlabel))))),

        linked_subsystem : TromPortTuple * set of Subsystem +> bool
        linked_subsystem(tptuple, subsystems) ==
           (exists1 s in set subsystems &
              (((linked_trom(tptuple, s.troms)) and
               (not linked_subsystem(tptuple, s.includes))) or
               ((not linked_trom(tptuple, s.troms)) and
                (linked_subsystem(tptuple, s.includes)))) and

            (forall s2 in set {su | su : Subsystem &
               su in set subsystems and su <> s} &
               ((not linked_trom(tptuple, s2.troms)) and
                (not linked_subsystem(tptuple, s2.includes))))) in

      (forall pl in set portlinks &
         ((((linked_trom(pl.tromporttuple1, troms)) and
            (not linked_subsystem(pl.tromporttuple1, includes))) or
           ((not linked_trom(pl.tromporttuple1, troms)) and
            (linked_subsystem(pl.tromporttuple1, includes)))) and
          (((linked_trom(pl.tromporttuple2, troms)) and
            (not linked_subsystem(pl.tromporttuple2, includes))) or
           ((not linked_trom(pl.tromporttuple2, troms)) and
            (linked_subsystem(pl.tromporttuple2, includes)))))))

\end{vdm_al}

\begin{vdm_al}

state System of

SUBSYSTEM : Subsystem

SIMULATIONEVENTLIST : seq of SimulationEvent

LSLLIBRARY : set of LSLTraitDefinition

CLOCK : nat

inv mk_System(subsystem, simulationeventlist, lsllibrary, clock) ==

   (let contains_trom : Subsystem +> bool
        contains_trom(subsys) ==
           ((subsys.troms <> { }) or
           (exists1 s in set subsys.includes & (contains_trom(s))))
    in

      contains_trom(subsystem)) and

   (let contains_portlink : Subsystem +> bool
        contains_portlink(subsys) ==
           ((subsys.portlinks <> { }) or
           (exists1 s in set subsys.includes & (contains_portlink(s))))
    in

      contains_portlink(subsystem)) and

   (forall i, j in set inds simulationeventlist &
      (((i = j) and (simulationeventlist(i) = simulationeventlist(j)))or
       ((i < j) and (simulationeventlist(i).occurtime <=
                     simulationeventlist(j).occurtime)) or
       ((i > j) and (simulationeventlist(i).occurtime >=
                     simulationeventlist(j).occurtime)))) and

   (forall se1, se2 in set elems simulationeventlist &
      (((se1.occurtime = se2.occurtime) and
        (se1.tromlabel <> se2.tromlabel)) or
       (se1.occurtime <> se2.occurtime))) and

   (let accepted_by_trom : SimulationEvent * Subsystem +> bool
        accepted_by_trom(se, subsys) ==
           (exists1 trom in set subsys.troms &
              ((trom.label = se.tromlabel) and
               (exists1 e in set trom.events &
                   ((e.label = se.eventlabel) and
                    (exists1 pt in set trom.porttypes &
                       ((pt = e.porttype) and
                        (exists1 p in set elems pt.portlist &
                           (p.label = se.portlabel)))))))) in

    let accepted_by_subsystem : SimulationEvent * Subsystem +> bool
        accepted_by_subsystem(se, subsys) ==
           (exists1 s in set subsys.includes &
              ((((accepted_by_trom(se, s)) and
                 (not accepted_by_subsystem(se, s))) or
                ((not accepted_by_trom(se, s)) and
                 (accepted_by_subsystem(se, s)))) and
               (forall s2 in set {su | su : Subsystem &
                  su in set subsys.includes and su <> s} &
                ((not accepted_by_trom(se, s2)) and
                 (not accepted_by_subsystem(se, s2)))))) in

      (forall se in set elems simulationeventlist &
         (((accepted_by_trom(se, subsystem)) and
          (not accepted_by_subsystem(se, subsystem))) or
          ((not accepted_by_trom(se, subsystem)) and
           (accepted_by_subsystem(se, subsystem)))))) and

   (let exists_lsltrait : Subsystem +> bool
        exists_lsltrait(subsys) ==
           ((forall trom in set subsys.troms &
               (forall tr in set trom.lsltraits &
                  (exists traitdef in set lsllibrary &
                     (traitdef.label = tr.traitlabel)))) and

            (forall s in set subsys.includes &
               (exists_lsltrait(s)))) in

       (exists_lsltrait(subsystem)))

init mk_System(subsys, simeventlist, lsllib, clock) ==

   simeventlist <> [] and clock = 0

end

\end{vdm_al}

\begin{vdm_al}

functions

   get_trom_object(tromlabel : String, subsystem : Subsystem) trom: [Trom]

   post

      ((trom in set subsystem.troms and trom.label = tromlabel) or

       (exists1 s in set subsystem.includes &

           (trom = get_trom_object(tromlabel, s))) or

       (trom = nil));

   get_transition_spec(trom : Trom, se : SimulationEvent) ts : [TransitionSpec]

   pre

      (trom.label = se.tromlabel)

   post

      (((ts in set trom.transitionspecs) and

        ((trom.currentstate.label = ts.sourcestate.label) or

         (substate_of(trom.currentstate, ts.sourcestate))) and

        (ts.triggerevent.label = se.eventlabel) and

        (ts.portcondition = true) and

        (ts.enabcondition = true)) or

       (ts = nil));

   substate_of : State * State +> bool
   substate_of(substate, complexstate) ==

      (substate in set complexstate.substates or

       (exists1 s in set complexstate.substates &

          (s.type = <COMPLEX> and substate_of(substate, s))))

   pre

      (complexstate.type = <COMPLEX>);

   get_entry_state(complexstate : State) entry : State

   pre

      (complexstate.type = <COMPLEX>)

   post

      (exists1 s in set complexstate.substates &

         ((s.isinitial = true) and

          ((s.type = <SIMPLE> and entry = s) or

           (s.type = <COMPLEX> and entry = get_entry_state(s)))));

   get_initial_state(trom : Trom) initial : State

   pre

      (trom.states <> { })

   post

      (exists1 s in set trom.states &

         ((s.isinitial = true) and

          ((s.type = <SIMPLE> and initial = s) or

           (s.type = <COMPLEX> and initial = get_entry_state(s)))));

   get_linked_tromport_tuple(tupleA : TromPortTuple, subsystem : Subsystem)
                             tupleB : [TromPortTuple]

   post

      ((exists1 pl in set subsystem.portlinks &

          ((pl.tromporttuple1 = tupleA and pl.tromporttuple2 = tupleB) or

           (pl.tromporttuple2 = tupleA and pl.tromporttuple1 = tupleB))) or

       (exists1 s in set subsystem.includes &

          (tupleB = get_linked_tromport_tuple(tupleA, s))) or

       (tupleB = nil));

   exists_in_subsystem : Trom * Subsystem +> bool
   exists_in_subsystem(trom, subsys) ==

      (trom in set subsys.troms or

       (exists1 subsystem in set subsys.includes &

          (exists_in_subsystem(trom, subsystem))))

   pre

      ((subsys.troms <> { }) or (subsys.includes <> { }));

   get_unconstrained_internal_event(trom : Trom) event : [Event]

   post

      ((exists ts in set trom.transitionspecs &

         ((ts.sourcestate = trom.currentstate) and

          (ts.triggerevent.type = <INTERNAL>) and

          (not constrained_event(trom, ts.triggerevent)) and

          (event = ts.triggerevent))) or

       (event = nil));

   constrained_event : Trom * Event +> bool
   constrained_event(trom, event) ==

      (exists tc in set trom.timeconstraints &

         (tc.constrainedevent = event))

   pre

      (event in set trom.events);

   get_simevent_index(se : SimulationEvent,
                      se_list : seq of SimulationEvent) index : nat1

   pre

      (se in set elems se_list)

   post

      (se_list(index) = se);

   get_random_time_within_rw(rw : ReactionWindow) time : nat

   post

      ((time >= rw.lowertimebound) and (time <= rw.uppertimebound));

   get_lru_port(portlist : seq of Port) port : Port

   pre

      (portlist <> [])

   post

      (port in set elems portlist)

operations

   simulator : () ==> ()
   simulator() ==
   (
      dcl i : nat1 := 1;

      initialize_simulation_clock();

      schedule_unconstrained_internal_events_from_initial_state();

      while (i <= len SIMULATIONEVENTLIST) do
      (
         while (CLOCK < SIMULATIONEVENTLIST(i).occurtime) do
         (
            update_simulation_clock()
         );

         while ((i <= len SIMULATIONEVENTLIST) and
                (CLOCK = SIMULATIONEVENTLIST(i).occurtime)) do
         (
            handle_event(SIMULATIONEVENTLIST(i));

            i := i + 1
         )
      )
   )

   pre

      ((SIMULATIONEVENTLIST <> []) and

       (forall se in set elems SIMULATIONEVENTLIST &

          ((se.occurtime >= CLOCK) and

           (se.eventhistory = nil))) and

       (forall trom in set {trom | trom : Trom &
                                   exists_in_subsystem(trom, SUBSYSTEM)} &

             ((trom.currentstate = get_initial_state(trom)) and

              (forall tc in set trom.timeconstraints &

                 (tc.reactionwindows = { })))))

   post

      ((SIMULATIONEVENTLIST <> []) and

       (SIMULATIONEVENTLIST(len SIMULATIONEVENTLIST).occurtime = CLOCK) and

       (forall se in set elems SIMULATIONEVENTLIST &

          ((se.occurtime <= CLOCK) and

           (se.eventhistory <> nil))) and

       (forall trom in set {trom | trom : Trom
                                 & exists_in_subsystem(trom, SUBSYSTEM)} &

             (forall tc in set trom.timeconstraints &

                (tc.reactionwindows = { }))));

   handle_event : SimulationEvent ==> ()
   handle_event(se) ==
   (
      dcl trom : [Trom],

          ts : [TransitionSpec];

      trom := get_trom_object(se.tromlabel, SUBSYSTEM);

      if trom = nil then return else skip;

      ts := get_transition_spec(trom, se);

      if ts = nil then
      (
         update_history_notransition(trom, se, ts)
      )
      else
      (
         update_history_assignment_vector(trom, se, ts);

         if ts.postcondition = false then
         (
            update_history_notransition(trom, se, ts)
         )
         else
         (
            update_history_transition(trom, se, ts);

            update_trom_current_state(trom, se, ts);

            handle_transition(trom, se, ts);

            schedule_unconstrained_internal_event(trom, se)
         )
      )
   )

   pre

      (se.occurtime = CLOCK)

   post

      (CLOCK = CLOCK~);

   handle_transition : Trom * SimulationEvent * TransitionSpec ==> ()
   handle_transition(trom, se, ts) ==
   (
      for all tc in set trom.timeconstraints do
      (
         if tc.constrainedevent.label = se.eventlabel then
         (
            for all rw in set tc.reactionwindows do
            (
               if se.occurtime >= rw.lowertimebound and
                  se.occurtime <= rw.uppertimebound then
               (
                  update_history_fire_reaction(trom, se, tc, rw);

                  fire_reaction(trom, se, tc, rw)
               )
            )
         );

         if trom.currentstate in set tc.disablingstates then
         (
            for all rw in set tc.reactionwindows do
            (
               update_history_disable_reaction(trom, se, tc, rw);

               disable_reaction(trom, se, tc, rw)
            )
         );

         if ts.label = tc.transition.label then
         (
            update_history_enable_reaction(trom, se, tc, ts);

            enable_reaction(trom, se, tc, ts)
         )
      )
   )

   pre

      (se.occurtime = CLOCK)

   post

      (CLOCK = CLOCK~);

   update_trom_current_state(trom : Trom, se : SimulationEvent,
                             ts : TransitionSpec)

   pre

      (ts.postcondition = true)

   post

      (((ts.destinstate.type = <SIMPLE>) and
        (trom.currentstate = ts.destinstate)) or

       ((ts.destinstate.type = <COMPLEX>) and
        (trom.currentstate = get_entry_state(ts.destinstate))));

   update_history_assignment_vector(trom : Trom, se : SimulationEvent,
                                    ts : [TransitionSpec])

   pre

      (ts <> nil)

   post

      (se.eventhistory.assignmentvector = trom.assignmentvector);

   update_history_notransition(trom : Trom, se : SimulationEvent,
                               ts : [TransitionSpec])

   pre

      ((ts = nil) or (ts.postcondition = false))

   post

      ((se.eventhistory.triggeredtransition = false) and

       (se.eventhistory.tromcurrentstate = nil) and

       (se.eventhistory.assignmentvector = nil) and

       (se.eventhistory.reactionshistory = { }));

   update_history_transition(trom : Trom, se : SimulationEvent,
                             ts : TransitionSpec)

   pre

      (ts.postcondition = true)

   post

      ((se.eventhistory.triggeredtransition = true) and

       (se.eventhistory.tromcurrentstate = trom.currentstate) and

       (se.eventhistory.assignmentvector = trom.assignmentvector) and

       (se.eventhistory.reactionshistory = { }));

   update_history_fire_reaction(trom : Trom, se : SimulationEvent,
                                tc : TimeConstraint,
         rw : ReactionWindow)

   pre

      ((tc.constrainedevent.label = se.eventlabel) and

       (rw in set tc.reactionwindows) and

       (se.occurtime >= rw.lowertimebound) and

       (se.occurtime <= rw.uppertimebound))

   post

      (exists rh in set se.eventhistory.reactionshistory &

         ((rh.timeconstraint = tc) and

          (rh.reactionwindow = rw) and

          (rh.reaction = <FIRED>)));

   update_history_disable_reaction(trom : Trom, se : SimulationEvent,
                                   tc : TimeConstraint,
         rw : ReactionWindow)

   pre

      ((trom.currentstate in set tc.disablingstates) and

       (rw in set tc.reactionwindows))

   post

      (exists rh in set se.eventhistory.reactionshistory &

         ((rh.timeconstraint = tc) and

          (rh.reactionwindow = rw) and

          (rh.reaction = <DISABLED>)));

   update_history_enable_reaction(trom : Trom, se : SimulationEvent,
                                  tc : TimeConstraint,
        ts : TransitionSpec)

   ext rd CLOCK : nat

   pre

      (ts.label = tc.transition.label)

   post

      (let rw : ReactionWindow be st

         rw = mk_ReactionWindow(tc.timebounds.lowertimebound + CLOCK,
                                tc.timebounds.uppertimebound + CLOCK) in

         (exists rh in set se.eventhistory.reactionshistory &

            ((rh.timeconstraint = tc) and

             (rh.reactionwindow = rw) and

             (rh.reaction = <ENABLED>))));

   fire_reaction(trom : Trom, se : SimulationEvent,
                 tc : TimeConstraint, rw : ReactionWindow)

   pre

      ((tc.constrainedevent.label = se.eventlabel) and

       (rw in set tc.reactionwindows) and

       (se.occurtime >= rw.lowertimebound) and

       (se.occurtime <= rw.uppertimebound))

   post

      (rw not in set tc.reactionwindows);

   disable_reaction(trom : Trom, se : SimulationEvent,
                    tc : TimeConstraint, rw : ReactionWindow)

   ext rd SUBSYSTEM : Subsystem

       wr SIMULATIONEVENTLIST : seq of SimulationEvent

   pre

      ((trom.currentstate in set tc.disablingstates) and

       (rw in set tc.reactionwindows))

   post

      ((rw not in set tc.reactionwindows) and

       (let se2 : SimulationEvent be st

          se2 = get_enabled_simevent(trom, tc) in

          (((tc.constrainedevent.type = <INTERNAL>) and

            (SIMULATIONEVENTLIST =
                                   [s | s in seq SIMULATIONEVENTLIST~ &
                                          s <> se2])) or

           ((tc.constrainedevent.type = <OUTPUT>) and

            (let tromporttuple : [TromPortTuple] be st

               tromporttuple = get_linked_tromport_tuple
                             (mk_TromPortTuple(se2.tromlabel, se2.portlabel),
                                SUBSYSTEM) in

            (let se3 : SimulationEvent be st

               se3 = get_enabled_simevent_synch(tromporttuple, tc) in

               SIMULATIONEVENTLIST =
                                     [s | s in seq SIMULATIONEVENTLIST~ &
                                          s <> se2 and
                                          s <> se3]))))));

   enable_reaction(trom : Trom, se : SimulationEvent,
                   tc : TimeConstraint, ts : TransitionSpec)

   ext rd CLOCK : nat

       rd SUBSYSTEM : Subsystem

       wr SIMULATIONEVENTLIST : seq of SimulationEvent

   pre

      (ts.label = tc.transition.label)

   post

      (let rw : ReactionWindow be st

         rw = mk_ReactionWindow(tc.timebounds.lowertimebound + CLOCK,
                                 tc.timebounds.uppertimebound + CLOCK) in

      (let port : Port be st

         port = get_lru_port(tc.constrainedevent.porttype.portlist) in

      (let occurtime : nat be st

         occurtime = get_random_time_within_rw(rw) in

      (let se2 : SimulationEvent be st

         se2 = mk_SimulationEvent
                         (tc.constrainedevent.label, trom.label,
                          port.label, occurtime, nil) in

         ((rw in set tc.reactionwindows) and

          (se2 in set elems SIMULATIONEVENTLIST) and

          (((tc.constrainedevent.type = <OUTPUT>) and

            (let tromporttuple : [TromPortTuple] be st

               tromporttuple = get_linked_tromport_tuple
                           (mk_TromPortTuple(se2.tromlabel,
                                             se2.portlabel), SUBSYSTEM) in

            (((tromporttuple <> nil) and

              (let se3 : SimulationEvent be st

               se3 = mk_SimulationEvent
                                 (se2.eventlabel,
                                  tromporttuple.tromlabel,
                                  tromporttuple.portlabel,
                                  se2.occurtime, nil) in

               (se3 in set elems SIMULATIONEVENTLIST))) or

             (tromporttuple = nil)))) or

           (tc.constrainedevent.type = <INTERNAL>)))))));

   pure get_enabled_simevent(trom : Trom, tc : TimeConstraint)
                        se : SimulationEvent

   ext rd CLOCK : nat

       rd SIMULATIONEVENTLIST : seq of SimulationEvent

   pre

      (tc in set trom.timeconstraints)

   post

      ((se in set elems SIMULATIONEVENTLIST) and

       (se.eventlabel = tc.constrainedevent.label) and

       (se.tromlabel = trom.label) and

       (se.occurtime >= CLOCK) and

       (se.eventhistory = nil));

   pure get_enabled_simevent_synch(tromporttuple : TromPortTuple,
                              tc : TimeConstraint) se : SimulationEvent

   ext rd CLOCK : nat

       rd SIMULATIONEVENTLIST : seq of SimulationEvent

   post

      ((se in set elems SIMULATIONEVENTLIST) and

       (se.eventlabel = tc.constrainedevent.label) and

       (se.tromlabel = tromporttuple.tromlabel) and

       (se.occurtime >= CLOCK) and

       (se.eventhistory = nil));

   schedule_unconstrained_internal_events_from_initial_state()

   ext rd CLOCK : nat

       rd SUBSYSTEM : Subsystem

       wr SIMULATIONEVENTLIST : seq of SimulationEvent

   pre

      CLOCK = 0

   post

      ((CLOCK = 0) and

       (forall trom in set {trom | trom : Trom
                                 & exists_in_subsystem(trom, SUBSYSTEM)} &

         (let event : [Event] = get_unconstrained_internal_event(trom) in

            (((event <> nil) and

              (let se : SimulationEvent be st

                 se = mk_SimulationEvent
                     (event.label, trom.label, "NULLPORT", CLOCK, nil) in

                 ((se in set elems SIMULATIONEVENTLIST) and

                  (let i : nat1 be st

                     SIMULATIONEVENTLIST(i) = se in

                   (forall se2 in set elems SIMULATIONEVENTLIST~ &

                      (let j : nat1 be st

                         SIMULATIONEVENTLIST(j) = se2 in

                       i < j)))))) or

             (event = nil)))));

   schedule_unconstrained_internal_event(trom : Trom, se : SimulationEvent)

   ext rd CLOCK : nat

       wr SIMULATIONEVENTLIST : seq of SimulationEvent

   pre

      ((se in set elems SIMULATIONEVENTLIST) and (se.tromlabel = trom.label))

   post

      (let event : [Event] = get_unconstrained_internal_event(trom) in

         (((event <> nil) and

           (let j : nat1 be st

              j = get_simevent_index(se, SIMULATIONEVENTLIST) in

           (let se2 : SimulationEvent be st

              se2 = mk_SimulationEvent
                     (event.label, trom.label, "NULLPORT", CLOCK, nil) in

              (SIMULATIONEVENTLIST =

                 [SIMULATIONEVENTLIST~(i)
                 | i in set inds SIMULATIONEVENTLIST~ & i <= j] ^
            [se2] ^
                    [SIMULATIONEVENTLIST~(i)
                    | i in set inds SIMULATIONEVENTLIST~ & i > j])))) or

          (event = nil)));

   initialize_simulation_clock()

   ext wr CLOCK : nat

   post

      CLOCK = 0;

   update_simulation_clock()

   ext wr CLOCK : nat

   post

      CLOCK = CLOCK~ + 1

end TROM

\end{vdm_al}

\end{document}

quality89%

¤ Dauer der Verarbeitung: 0.22 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.