No verification results generated when using Gauss-Seidel CTMC model

[Zhen Zhang]

Hello,

I've been using the Gauss-Seidel option to run PRISM on the attached genetic circuit CTMC model with the attached CSL property. But from the output (also attached), it did not seem to generate any verification results. I listed the memory setup information, PRISM version, and the command line below. 

Version: 4.5

Date: Fri Apr 03 23:40:17 MDT 2020

Hostname: el176-deeplearning

Memory limits: cudd=100g, java(heap)=80g

Command line: prism -gaussseidel -cuddmaxmem 100g Circuit0xE8_tmp.sm hazard.csl

Regards,
Zhen Zhang

[Dave Parker]

Hi Zhen,

It seems that both the number of states and the size of the symbolic
representation are very large. Both the symbolic and explicit engines
take a long time without making much progress. Do you have an idea how
large the model is? Perhaps, because your memory limits are set quite
high, you do not see a mem-out error/crash for a long time.

Best wishes,

Dave

> --
> You received this message because you are subscribed to the Google
> Groups "PRISM model checker developers" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to prismmodelchecke...@googlegroups.com
> <mailto:prismmodelchecke...@googlegroups.com>.
> To view this discussion on the web, visit
> https://groups.google.com/d/msgid/prismmodelchecker-dev/38b9e7e7-a8f9-4f50-86f4-43c82b75ccfe%40googlegroups.com
> <https://groups.google.com/d/msgid/prismmodelchecker-dev/38b9e7e7-a8f9-4f50-86f4-43c82b75ccfe%40googlegroups.com?utm_medium=email&utm_source=footer>.

[Zhen Zhang]

Dear Dave,

Thank you very much for getting back to me. Dr. Gethin Norman responded to my questions shortly after I posted them, too. Unfortunately, I do not have an estimate of the state size of this model. Actually, it turned out that this model was converted from an SBML model without applying the reaction-based quasi-steady-state abstraction. We have regenerated one with this abstraction, and have been able to use PRISM to model check CSL properties. 

There is another interesting problem for us to explore further. Our approach is to use our STAMINA tool (https://github.com/fluentverification/stamina) to truncate the explicit state space, and then send it to PRISM to perform CTMC analysis. STAMINA generated 2,826,140 states (1 initial) and 18,538,724 transitions on the non-abstracted model. Our observation is that the Gauss-Seidel and power methods  take long time (15+ hours) to do the CTMC analysis. The machine we used has a 24-core 3.5 GHz processor and 132 GB memory. The computer was stuck at 100% CPU and less than 20% memory usage for almost the entire duration of the CTMC analysis. It did not terminate due to insufficient memory after 15+ hours, either. But it was hard to pinpoint the issue because STAMINA calls PRISM.

Now STAMINA has the ability to save the state space to a file, we can decouple STAMINA's state generation from PRISM's CTMC analysis and hopefully get better diagnostic information. I will keep you updated on what we find.

Best,

Zhen

--

Zhen Zhang