= 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 B models and you need to copy the plantUML.jar file to ProB's lib folder.
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:
-->
->
->x
->>
etc
Optionally you can add these suffixes:
++(activate the target)
-(deactivate source)
**(create an instance of target)
!!(destroy an instance of target)