Re: ARC model specified in spinroot/promela

Am 2023-09-02 12:47, schrieb Mathew, Cherry G.*:
> 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.

And just when I've send the mail, it finished... :)
---snip---
Samstag, 02. September 2023, 18:51:21
(203) root@ttypts/1 # time make spin-gen
cp arc.pml model #mimic modex
cat arc.drv > spinmodel.pml;cat model >> spinmodel.pml;cat arc.inv >> 
spinmodel.pml;
spin -a spinmodel.pml
ltl ltl_0: ((<> ([] ((_nr_pr==1)))) && ([] (((((len(T1.item_list)<=5)) 
&& ((len(B1.item_list)<=5))) && ((len(T2.item_list)<=5))) && 
((len(B2.item_list)<=5))))) && (<> ((p>0)))
make spin-gen  0,04s user 0,11s system 24% cpu 0,585 total

Samstag, 02. September 2023, 18:51:29
(204) root@ttypts/1 # time make spin-build
cc -o pan pan.c
make spin-build  0,47s user 0,26s system 56% cpu 1,286 total

Samstag, 02. September 2023, 18:51:37
(205) root@ttypts/1 # time make spin-run
cc -o pan pan.c
./pan -a #Generate arc.pml.trail        on error
Depth=     271 States=    1e+06 Transitions= 2.04e+06 Memory=   194.550 
t=     4.47 R=   2e+05
Depth=     271 States=    2e+06 Transitions= 4.09e+06 Memory=   264.081 
t=     9.16 R=   2e+05
Depth=     271 States=    3e+06 Transitions= 6.16e+06 Memory=   334.101 
t=     13.5 R=   2e+05
Depth=     271 States=    4e+06 Transitions= 8.25e+06 Memory=   410.370 
t=     18.4 R=   2e+05
Depth=     271 States=    5e+06 Transitions= 1.04e+07 Memory=   485.272 
t=     23.4 R=   2e+05
Depth=     271 States=    6e+06 Transitions= 1.25e+07 Memory=   560.175 
t=       28 R=   2e+05
Depth=     271 States=    7e+06 Transitions= 1.46e+07 Memory=   635.077 
t=     33.1 R=   2e+05
Depth=     271 States=    8e+06 Transitions= 1.67e+07 Memory=   710.077 
t=       38 R=   2e+05
Depth=     271 States=    9e+06 Transitions= 1.88e+07 Memory=   787.812 
t=     43.2 R=   2e+05
Depth=     271 States=    1e+07 Transitions= 2.09e+07 Memory=   867.987 
t=     48.5 R=   2e+05
Depth=     271 States=  1.1e+07 Transitions=  2.3e+07 Memory=   948.163 
t=     53.5 R=   2e+05
Depth=     271 States=  1.2e+07 Transitions= 2.51e+07 Memory=  1028.339 
t=     58.7 R=   2e+05
Depth=     271 States=  1.3e+07 Transitions= 2.72e+07 Memory=  1108.515 
t=     63.8 R=   2e+05
Depth=     271 States=  1.4e+07 Transitions= 2.93e+07 Memory=  1188.202 
t=     69.1 R=   2e+05
Depth=     271 States=  1.5e+07 Transitions= 3.15e+07 Memory=  1267.401 
t=     74.5 R=   2e+05
Depth=     271 States=  1.6e+07 Transitions= 3.36e+07 Memory=  1346.503 
t=     79.9 R=   2e+05
Depth=     271 States=  1.7e+07 Transitions= 3.58e+07 Memory=  1425.605 
t=     85.2 R=   2e+05
[...]
Depth=     271 States= 2.07e+08 Transitions= 4.44e+08 Memory= 20175.351 
t= 1.22e+03 R=   2e+05
Depth=     271 States= 2.08e+08 Transitions= 4.46e+08 Memory= 20262.558 
t= 1.22e+03 R=   2e+05
Depth=     271 States= 2.09e+08 Transitions= 4.49e+08 Memory= 20349.667 
t= 1.23e+03 R=   2e+05
pan:1: acceptance cycle (at depth 270)
pan: wrote spinmodel.pml.trail

(Spin Version 6.5.0 -- 1 July 2019)
Warning: Search not completed
         + 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 184 byte, depth reached 271, errors: 1
1.0465042e+08 states, stored (2.09301e+08 visited)
2.4007432e+08 states, matched
4.4937506e+08 transitions (= visited+matched)
  44667618 atomic steps
hash conflicts:  63844226 (resolved)

Stats on memory usage (in Megabytes):
21158.112       equivalent memory usage for states (stored*(State-vector 
+ overhead))
18344.457       actual memory usage for states (compression: 86.70%)
                 state-vector as stored = 156 byte + 28 byte overhead
  2048.000       memory used for hash table (-w28)
     0.534       memory used for DFS stack (-m10000)
    17.170       memory lost to fragmentation
20375.839       total actual memory usage



pan: elapsed time 1.23e+03 seconds
pan: rate 169922.52 states/second
make spin-run  1199,05s user 34,46s system 99% cpu 20:33,94 total
---snip---

Hope this helps,
Alexander.

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