Re: ARC model specified in spinroot/promela

>>>>> Alexander Leidinger <Alexander@Leidinger.net> writes:


[...]


    > Seems to be single threaded (Adrian, this is with spin 6.5.0 from
    > an about 2 days old ports tree). Takes only 1 CPU. After 20min it
    > is at 25G (20G RES). The system has 64G of RAM and 100G of swap,
    > we will see if this is enough.

Thank you so much for this, and the trace output in the subsequent
email!

So there's room for improvement in my Makefile to:

1) Explore multithreaded/CPU
2) Understand state space explosion scale - it is exponential to the
   number of processes, I've fixed it to run in a loop - will report
   back once I have good progress also with the model extraction part.
3) My model has errors - I'm glad to see that the error reporting is the
   same in my new optimised loop, as in the RAM hungry version you ran.

Thanks once again - this is very helpful. I will report back once I have
more progress.

-- 
~cherry