[Verifpal] generating sequence diagrams?

Nadim Kobeissi nadim at symbolic.software
Tue Apr 28 18:51:09 CEST 2020


For Snap, we figured out a fix: just set your verifpal.path to "/snap/verifpal/current/bin/verifpal” in the user config.

The typo in example.vp was already fixed in Verifpal 0.13.2, released today.

Also make sure you’re using version 1.0.6 of the VSCode extension.

Nadim Kobeissi
Symbolic Software • https://symbolic.software

> On 27 Apr 2020, at 10:03 PM, Marko Schuetz-Schmuck <markoschuetz at googlemail.com> wrote:
> 
> Dear Nadim,
> 
> OK, seems I'm getting somewhere now.
> 
> 1. The snap installed verifpal does not give me the protocol diagram,
> neither the popups.
> 2. The verifpal from the 0.13.1 zip file does give me both, but....
> 3. the simple.vp example file contains a typo: an excess a at the end of
> line 16. I was only after I spotted that, that I got the protocol
> diagram.
> 
> Thanks a lot for helping me figure this out,
> 
> Marko
> Nadim Kobeissi <nadim at symbolic.software> writes:
> 
>> Dear Marko,
>> 
>> You are most likely inputting an invalid Verifpal model. If you try to
>> visualize for example simple.vp, I bet it will work:
>> https://source.symbolic.software/verifpal/verifpal/-/blob/master/examples/simple.vp
>> 
>> 
>> I just pushed an update to the Visual Studio Code extension, version 1.0.4,
>> that will give more clear errors when the user attempts to either visualize
>> or analyze an invalid model.
>> 
>> Also, please make sure Verifpal is installed on your computer and that it
>> is detected by Visual Studio Code through your PATH. If it's not, you can
>> set the path to the Verifpal manually using the `verifpal.path` option in
>> your Visual Studio Code user settings file.
>> 
>> (You can easily test whether Verifpal is recognized by Visual Studio Code
>> by opening simple.vp, hovering your cursor over a constant and checking
>> whether Visual Studio Code correctly maps it back to its values in the
>> hover popup, or by attempting to generate a diagram of simple.vp, etc. etc.)
>> 
>> Nadim Kobeissi
>> Symbolic Software • https://symbolic.software
>> Sent from office
>> 
>> 
>> On Sun, Apr 26, 2020 at 9:56 PM Marko Schuetz-Schmuck <
>> markoschuetz at googlemail.com> wrote:
>> 
>>> Nadim Kobeissi <nadim at symbolic.software> writes:
>>> 
>>> Thanks! But I still cannot get it: I installed the Verifpal extension
>>> for VS code and I have the corresponding entries in the command palette,
>>> but when I open Verifpal Protocol Diagram another pane opens, but
>>> remains black.
>>> 
>>> Any ideas?
>>> 
>>> Thanks and best regards,
>>> 
>>> Marko
>>> 
>>>> This was made using the same diagram generator that you can find and use
>>> yourself within the Verifpal extension for Visual Studio Code:
>>>> 
>>>> 
>>> https://marketplace.visualstudio.com/items?itemName=symbolicsoft.verifpal
>>>> 
>>>> Nadim Kobeissi
>>>> Symbolic Software • https://symbolic.software
>>>> 
>>>>> On 25 Apr 2020, at 8:07 PM, Marko Schuetz-Schmuck <
>>> markoschuetz at googlemail.com> wrote:
>>>>> 
>>>>> Dear Nadim,
>>>>> 
>>>>> e.g. the one on page 10 corresponding to the simple protocol.
>>>>> 
>>>>> Best regards,
>>>>> 
>>>>> Marko
>>>>> 
>>>>> Nadim Kobeissi <nadim at symbolic.software> writes:
>>>>> 
>>>>>> Dear Marko,
>>>>>> 
>>>>>> Could you please point out a sequence diagram in particular?
>>>>>> 
>>>>>> Thank you,
>>>>>> 
>>>>>> Nadim Kobeissi
>>>>>> Symbolic Software • https://symbolic.software
>>>>>> 
>>>>>>> On 25 Apr 2020, at 3:44 PM, Marko Schütz-Schmuck via Verifpal
>>> <verifpal at lists.symbolic.software> wrote:
>>>>>>> 
>>>>>>> Hi
>>>>>>> 
>>>>>>> I was wondering if the sequence diagrams in the Verifpal manual were
>>> generated automatically from the textual description. Or if not, which to
>>> was used to generate then?
>>>>>>> 
>>>>>>> Thanks and best regards
>>>>>>> 
>>>>>>> Marko
>>>>>>> 
>>>>>>> _______________________________________________
>>>>>>> Verifpal mailing list
>>>>>>> Verifpal at lists.symbolic.software
>>>>>>> https://lists.symbolic.software/mailman/listinfo/verifpal
>>>>>> 
>>>>> 
>>>>> --
>>>>> Prof. Dr. Marko Schütz-Schmuck
>>>>> Department of Computer Science and Engineering
>>>>> University of Puerto Rico at Mayagüez
>>>>> Mayagüez, PR 00681
>>>> 
>>> 
>>> --
>>> Prof. Dr. Marko Schütz-Schmuck
>>> Department of Computer Science and Engineering
>>> University of Puerto Rico at Mayagüez
>>> Mayagüez, PR 00681
>>> 
> 
> --
> Prof. Dr. Marko Schütz-Schmuck
> Department of Computer Science and Engineering
> University of Puerto Rico at Mayagüez
> Mayagüez, PR 00681

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: Message signed with OpenPGP
URL: <https://lists.symbolic.software/pipermail/verifpal/attachments/20200428/ebce901f/attachment.sig>


More information about the Verifpal mailing list