(Created page with "= UML Sequence Charts for Traces ProB has a new experimental feature to generate a UML sequence chart from the current animation trace. It currently only works for classical...") |
|||
(16 intermediate revisions by the same user not shown) | |||
Line 1: | Line 1: | ||
= | === 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 | It currently only works for classical B models and you need to copy the [https://plantuml.com/download plantuml.jar] file to ProB's lib folder. The file should be named plantuml.jar (without any version numbers). | ||
The feature is currently only available in ProB Tcl/Tk. | |||
=== Specifying the Actors | === Using the Command === | ||
It is available in the Visualize menu: | |||
[[file:ProBUMLSeqChartCmd.png|center||300px]] | |||
=== Specifying the Actors === | |||
For every B Operation Op that you want to visualise you need to add a definition | For every B Operation Op that you want to visualise you need to add a definition | ||
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. | ||
* 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: | Currently these arrow styles are supported: | ||
* | * '''-->''' | ||
* < | * '''->''' | ||
* | * '''->x''' | ||
* | * '''->>''' | ||
* '''-\\''' | |||
* '''\\\\-''' | |||
* '''//--''' | |||
* '''->o''' | |||
* '''o\\\\--''' | |||
* '''<->''' | |||
* '''<->o''' | |||
* '''-[#green]>''' | |||
* '''-[#green]->''' | |||
* '''-[#blue]->''' | |||
* '''-[#red]->''' | |||
* '''-[#red]>''' | |||
* '''-[#0000FF]->''' | |||
* '''<-''' | |||
* '''<--''' | |||
Optionally you can add these suffixes: | Optionally you can add these suffixes: | ||
* | * '''++''' (activate the target) | ||
* | * '''--''' (deactivate source) | ||
* | * '''**''' (create an instance of target) | ||
* <pre>!!</ | * '''!!''' (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> |
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 currently only available in ProB Tcl/Tk.
It is available in the Visualize menu:
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
Currently these arrow styles are supported:
Optionally you can add these suffixes:
The following diagram can be created using the model below after animating and then using the command above.
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