Re: ARC model specified in spinroot/promela

Am 2023-09-04 12:49, schrieb Mathew, Cherry G.*:
>>>>>> Mathew, Cherry G * <c@bow.st> writes:
> 
> [...]
> 
>     > 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.
> 
> Hi Again,
> 
> So just wanted to report back with a patch (absolute patch, not 
> relative,
> so please nuke your existing arc/ if you tried the old one and apply in
> a clean new subdirectory) on the following:

# make spin-run
cp arc.pml model #mimic modex
cat model > spinmodel.pml;cat arc.drv >> spinmodel.pml;cat arc.inv >> 
spinmodel.pml;
spin -am spinmodel.pml
ltl ltl_0: (((((((((<> ([] ((_nr_pr==1)))) && ([] 
(((((len(T1.item_list)+len(B1.item_list))+len(T2.item_list))+len(B2.item_list))<=(2*64))))) 
&& ([] (((len(T1.item_list)+len(B1.item_list))<=64)))) && ([] 
(((len(T2.item_list)+len(B2.item_list))<(2*64))))) && ([] 
(((len(T1.item_list)+len(T2.item_list))<=64)))) && ([] ((! 
(((((len(T1.item_list)+len(B1.item_list))+len(T2.item_list))+len(B2.item_list))<64))) 
|| (((len(B1.item_list)==0)) && ((len(B2.item_list)==0)))))) && ([] ((! 
(((((len(T1.item_list)+len(B1.item_list))+len(T2.item_list))+len(B2.item_list))>=64))) 
|| (((len(T1.item_list)+len(T2.item_list))==64))))) && ([] ((p<=64)))) 
&& (<> (((len(T1.item_list)==p)) && ((len(T2.item_list)==(64-p)))))) && 
(<> ((p>0)))
cc -DVECTORSZ=65536 -o pan pan.c
./pan -a #Generate arc.pml.trail        on error
error: max search depth too small

(Spin Version 6.5.0 -- 1 July 2019)
         + Partial Order Reduction

Full statespace search for:
         never claim             + (ltl_0)
         assertion violations    + (if within scope of claim)
         acceptance   cycles     + (fairness disabled)
         invalid end states      - (disabled by never claim)

State-vector 2124 byte, depth reached 9999, errors: 0
         1 states, stored
        11 states, matched
        12 transitions (= stored+matched)
    109989 atomic steps
hash conflicts:         0 (resolved)

Stats on memory usage (in Megabytes):
     0.002       equivalent memory usage for states (stored*(State-vector 
+ overhead))
    12.456       actual memory usage for states
   128.000       memory used for hash table (-w24)
     0.534       memory used for DFS stack (-m10000)
     5.686       memory lost to fragmentation
   140.500       total actual memory usage


unreached in init
         spinmodel.pml:80, state 28, "D_STEP80"
         spinmodel.pml:80, state 53, "D_STEP80"
         spinmodel.pml:154, state 70, "B1.item_list?_"
         spinmodel.pml:80, state 79, "D_STEP80"
         spinmodel.pml:90, state 85, "D_STEP90"
         spinmodel.pml:78, state 86, 
"(((len(T1.item_list)!=0)&&((len(T1.item_list)>p)||(B2.item_list??[eval(x[x_iid].iid)]&&(len(T1.item_list)==p)))))"
         spinmodel.pml:78, state 86, "else"
         spinmodel.pml:73, state 88, "D_STEP73"
         spinmodel.pml:159, state 90, "assert((len(B1.item_list)==0))"
         spinmodel.pml:160, state 94, "D_STEP160"
         spinmodel.pml:152, state 95, "((len(T1.item_list)<64))"
         spinmodel.pml:152, state 95, "else"
         spinmodel.pml:183, state 100, "B2.item_list?_"
         spinmodel.pml:198, state 128, "(1)"
         spinmodel.pml:268, state 155, "-end-"
         (13 of 155 states)
unreached in claim ltl_0
         _spin_nvr.tmp:70, state 108, "-end-"
         (1 of 108 states)

pan: elapsed time 0.164 seconds
pan: rate 6.0952381 states/second



No trail file generated...

Bye,
Alexander.

-- 
http://www.Leidinger.net Alexander@Leidinger.net: PGP 0x8F31830F9F2772BF
http://www.FreeBSD.org    netchild@FreeBSD.org  : PGP 0x8F31830F9F2772BF