Generating UML Sequence Charts: Difference between revisions

 
(14 intermediate revisions by one other user not shown)
Line 1: Line 1:
= UML Sequence Charts for Traces
=== Installation and Using ===


ProB has a new experimental feature to generate a UML sequence chart from the current animation trace.
ProB has a new experimental feature to generate a UML sequence chart from the current animation trace using [https://plantuml.com PlantUML].
It currently only works for classical B models and you need to copy the plantUML.jar file to ProB's lib folder.
It currently only works for classical B models and you need to copy the [https://plantuml.com/download plantuml.jarfile to ProB's lib folder. The file should be named plantuml.jar (without any version numbers).


The feature is available in ProB CLI, ProB Tcl/Tk and ProB2-UI.
=== Using the Command ===
It is available in the Visualize menu:
[[file:ProBUMLSeqChartCmd.png|center||300px]]


=== Specifying the Actors ===
=== Specifying the Actors ===
Line 13: Line 20:


The definition should either return
The definition should either return
* the empty string, meaning this operation should be ignored
* a couple (ActorFrom,ActorTo) specifying the name of the actor sending the message (ActorFrom) and the one receiving the message (ActorTo). You can use strings or other values (which will be converted to strings).
* a couple (ActorFrom,ActorTo) specifying the name of the actor sending the message (ActorFrom) and the one receiving the message (ActorTo). You can use strings or other values (which will be converted to strings).
* a triple (ActorFrom,ArrowStyle,ActorTo), where the actors are like above and ArrowStyle is a string representing a valid plantUML arrow.
* a triple (ActorFrom,ArrowStyle,ActorTo), where the actors are like above and ArrowStyle is a string representing a valid plantUML arrow.
Line 22: Line 30:
* '''->x'''
* '''->x'''
* '''->>'''
* '''->>'''
etc
* '''-\\'''
* '''\\\\-'''
* '''//--'''
* '''->o'''
* '''o\\\\--'''
* '''<->'''
* '''<->o'''
* '''-[#green]>'''
* '''-[#green]->'''
* '''-[#blue]->'''
* '''-[#red]->'''
* '''-[#red]>'''
* '''-[#0000FF]->'''
* '''<-'''
* '''<--'''


Optionally you can add these suffixes:
Optionally you can add these suffixes:
Line 29: Line 51:
* '''**''' (create an instance of target)
* '''**''' (create an instance of target)
* '''!!''' (destroy an instance of target)
* '''!!''' (destroy an instance of target)
== Example ==
The following diagram can be created using the model below after animating and then using the command above.
[[file:ProBUMLSeqCharScheduler.png|center||300px]]
And here is the well-known scheduler example with example SEQUENCE_CHART definitions:
<pre>
MACHINE scheduler_UML
SETS
PID  = {process1,process2,process3}
VARIABLES active, ready, waiting
DEFINITIONS
      "CHOOSE.def";
      SEQUENCE_CHART_INITIALISATION == ""; // ignore
      SEQUENCE_CHART_new(pp) == ("Master", "-->","**",pp);
      SEQUENCE_CHART_del(pp) == ("Master", "-->","!!",pp);
      SEQUENCE_CHART_ready(pp) == (pp, "-->","Master");
      SEQUENCE_CHART_swap == ("Master", "-->","--",CHOOSE(active))
INVARIANT
          active <: PID &
          ready <: PID  &
          waiting <: PID &
          (ready /\ waiting) = {} &
          active /\ (ready \/ waiting) = {} &
          /*@label "SAF" */ card(active) <= 1 &
          ((active = {})  => (ready = {}))
INITIALISATION
active := {} || ready := {} || waiting := {}
OPERATIONS
new(pp) =
SELECT
pp : PID  &
pp /: active &
pp /: (ready \/ waiting)
THEN
waiting := (waiting \/ { pp })
END;
del(pp) =
SELECT
pp : waiting
THEN
waiting := waiting - {pp}
END;
ready(rr) =
        SELECT
                rr : waiting
        THEN
                waiting := (waiting - {rr}) ||
                IF (active = {}) THEN
                  active := {rr}
                ELSE
                  ready := ready \/ {rr}
                END
        END;
swap =
        SELECT
                active /= {}
        THEN
                waiting := (waiting \/ active) ||
                IF (ready = {}) THEN
                  active := {}
                ELSE
                  ANY pp WHERE pp : ready
                  THEN
                      active := {pp} ||
                      ready := ready - {pp}
                  END
                END
        END
END
</pre>

Latest revision as of 12:39, 3 June 2024

Installation and Using

ProB has a new experimental feature to generate a UML sequence chart from the current animation trace using PlantUML. It currently only works for classical B models and you need to copy the plantuml.jar file to ProB's lib folder. The file should be named plantuml.jar (without any version numbers).

The feature is available in ProB CLI, ProB Tcl/Tk and ProB2-UI.

Using the Command

It is available in the Visualize menu:

ProBUMLSeqChartCmd.png

Specifying the Actors

For every B Operation Op that you want to visualise you need to add a definition

SEQUENCE_CHART_Op

in your DEFINITIONS. The definition can take arguments, in which case the actual arguments in the trace are passed to the definition. The definition can take fewer arguments (but not more) than the B operation.

The definition should either return

  • the empty string, meaning this operation should be ignored
  • a couple (ActorFrom,ActorTo) specifying the name of the actor sending the message (ActorFrom) and the one receiving the message (ActorTo). You can use strings or other values (which will be converted to strings).
  • a triple (ActorFrom,ArrowStyle,ActorTo), where the actors are like above and ArrowStyle is a string representing a valid plantUML arrow.
  • a triple (ActorFrom,ArrowStyle,ArrowSuffix,ActorTo), where the actors and arrow style are like above and ArrowSuffix is a string representing a valid plantUML arrow suffix.

Currently these arrow styles are supported:

  • -->
  • ->
  • ->x
  • ->>
  • -\\
  • \\\\-
  • //--
  • ->o
  • o\\\\--
  • <->
  • <->o
  • -[#green]>
  • -[#green]->
  • -[#blue]->
  • -[#red]->
  • -[#red]>
  • -[#0000FF]->
  • <-
  • <--

Optionally you can add these suffixes:

  • ++ (activate the target)
  • -- (deactivate source)
  • ** (create an instance of target)
  • !! (destroy an instance of target)

Example

The following diagram can be created using the model below after animating and then using the command above.

ProBUMLSeqCharScheduler.png

And here is the well-known scheduler example with example SEQUENCE_CHART definitions:

MACHINE scheduler_UML
SETS
	PID  = {process1,process2,process3}
VARIABLES active, ready, waiting
DEFINITIONS
      "CHOOSE.def";
      SEQUENCE_CHART_INITIALISATION == ""; // ignore
      SEQUENCE_CHART_new(pp) == ("Master", "-->","**",pp);
      SEQUENCE_CHART_del(pp) == ("Master", "-->","!!",pp);
      SEQUENCE_CHART_ready(pp) == (pp, "-->","Master");
      SEQUENCE_CHART_swap == ("Master", "-->","--",CHOOSE(active))
INVARIANT
           active <: PID &
           ready <: PID   &
           waiting <: PID &
           (ready /\ waiting) = {} &
           active /\ (ready \/ waiting) = {} &
           /*@label "SAF" */ card(active) <= 1 &
           ((active = {})  => (ready = {}))
INITIALISATION
	active := {} || ready := {} || waiting := {}
OPERATIONS
new(pp) =
	SELECT
		pp : PID  &
		pp /: active &
		pp /: (ready \/ waiting)
	THEN
		waiting := (waiting \/ { pp })
	END;
del(pp) =
	SELECT
		pp : waiting
	THEN
		waiting := waiting - {pp}
	END;
ready(rr) =
        SELECT
                rr : waiting
        THEN
                waiting := (waiting - {rr}) ||
                IF (active = {}) THEN
                   active := {rr}
                ELSE
                   ready := ready \/ {rr}
                END
        END;
swap =
        SELECT
                active /= {}
        THEN
                waiting := (waiting \/ active) ||
                IF (ready = {}) THEN
                   active := {}
                ELSE
                   ANY pp WHERE pp : ready
                   THEN
                       active := {pp} ||
                       ready := ready - {pp}
                   END
                END
        END
END