Re: ARC model specified in spinroot/promela

Hi Alexander,

>>>>> "AL" == Alexander Leidinger <Alexander@Leidinger.net> writes:


[...]


    AL> How long is this supposed to take? For me it took about 2
    AL> seconds to finish.

Apologies, I should have given more detailed instructions.

I've organised the process in three steps:

1) Generate the model from spec: make spin-gen
2) Build the model: make spin-build
3) Run the model: make spin-run

This is the heavy duty part, which takes up quite a bit of vmem (my
process dies at about 8GB due to lack of swap etc. - makes no sense to
thrash it beyond that without RAM - it slows down a lot).

If all goes well with step 3) , then you will see a summary of the run
on console. However, if there was an inconsistency or error detected in
the run, then a tracefile is generated (spinmodel.pml.trail). I've
included a target to dump a human friendly version of this trace.

4) Print trace from debug trail: make spin-trace


    AL> Note, the Makefile specifies a NetBSD src directory which I
    AL> don't have on this FreeBSD system...

Sorry, I should have mentioned - you can safely ignore that - no
specific external source layout is currently assumed - in fact I run
these tests on a Linux VM at the moment.

The source files become relevant only when the "model extraction" is
done - I haven't got there yet for this project.

>>>>> "ade" == Adriaan de Groot <adridg@freebsd.org> writes:

    ade> For what it's worth, spin is available from ports (devel/spin),
    ade> which I've just adopted and updated to 6.5.2, so it is quite
    ade> straightforward to get this running on any recent FreeBSD
    ade> system.

Hi ade,

Nice! I'd be curious to know performance comparisons viz Linux etc. esp
because there seems to be a threaded version of spin (not sure if the
FreeBSD package build enables this).

    ade> I tested only with the ancient Peterson's mutual exclusion,
    ade> which resolves instantly. Mailing-list archives don't preserve
    ade> attachments, so, Cherry, if you could send it me directly that
    ade> would be lovely. I spotted A. Mader's PLC Controller in the
    ade> SPIN documents, that is one I am familiar with, and then
    ade> realised that academic papers from the 2000s don't come with
    ade> source code :(

Thanks, I noticed that after checking the archives, and did send a
second mail with an inline patch. Will also send you a private one after
this.

Thanks so much for your interest - mainly, I'd like to understand how
bad the statespace explosion is for this model. This will help me get a
sense of what complexity of models we can attempt to verify like this,
with current "commodity" hardware.

Many Thanks,
-- 
~cherry