search

REPROSEC / dolev-yao-star-extrinsic

DY* with extrinsic proofs
https://reprosec.org/
Mozilla Public License 2.0
8 stars 0 forks source link

Feature: Printing Debug Trace #4

Closed fabian-hk closed 1 month ago

fabian-hk commented 2 months ago

This PR extends certain trace functions with print statements to generate debug traces from a protocol run. This helps to verify the correctness of a model. The trace is printed in JSON format, which allows the generation of Plantuml sequence diagrams with the following tool: https://github.com/fabian-hk/dolev-yao-star-output-parser. Note that this is currently a simple Python script which only works with protocols that involve 2 participants. An example diagram generated from the NSL model can be seen in the following image:

DY_Example_NSL_Debug native

Additionally, this PR adds support for the VS Code F* Extension by adding the file .fst.config.json to the root of the project.

fabian-hk commented 2 months ago

I like your suggestion with the trace_to_string function. I will implement it and update this PR.

fabian-hk commented 2 months ago

I am not yet ready to merge because I am currently trying to implement a version of trace_to_string that can take custom functions to convert messages, states, and events to a string.

fabian-hk commented 1 month ago

@TWal, are you working on this, or should I change the argument order?

TWal commented 1 month ago

Sorry I have been distracted by something else, will do that!