Re: ARC model specified in spinroot/promela
- In reply to: Dag-Erling_Smørgrav : "Re: ARC model specified in spinroot/promela"
- Go to: [ bottom of page ] [ top of archives ] [ this month ]
Date: Mon, 04 Sep 2023 15:59:41 UTC
>>>>> Dag-Erling Smørgrav <des@FreeBSD.org> writes:
> "Mathew, Cherry G.*" <c@bow.st> writes:
>> I'm hoping that someone can help me complete the current run, as
>> I don't have the computing resources required to run the full
>> model (about 16GB RAM).
> 16 GB is not a huge amount of memory. Would it help if you had
> access to a jail or VM with enough memory to run the model
> yourself?
Hi DES,
You probably caught up on the rest of the thread - I figured out a way
to reduce the state space explosion (it's got to do with how
spin/promela semantics map to regular function style languages) - in the
end, it all came down to just around a second runtime. I think the
complexity will remain there, until I improve it for
re-entrancy/concurrency/multi-threaded use.
(currently the code/model assumes no re-entry).
I will fall back on your offer if it becomes unmanageable then.
Many Thanks,
--
~cherry