Dynamic creation of processes in 4.1.24 won't work

[Happy Cookie]

Hi, 

I want to use dynamic creation of processes, but when I want to Spawn new, it ends with error "Spawn supported in SMC". I thought that development of SMC stopped and basic Uppaal has SMC features. When I want to download SMC version of Uppaal it redirects me to uppaal.org. Does anyone know how to solve this? Thank You

[Marius Mikučionis]

Dear Happy Cookie,

On Thursday, December 19, 2019 at 8:05:27 PM UTC+1, Happy Cookie wrote:

Hi, 

I want to use dynamic creation of processes, but when I want to Spawn new, it ends with error "Spawn supported in SMC". I thought that development of SMC stopped and basic Uppaal has SMC features. When I want to download SMC version of Uppaal it redirects me to uppaal.org. Does anyone know how to solve this? Thank You

Here is a brief status:

1) SMC has been integrated into development branch of Uppaal 4.1. There is no separate SMC anymore.

2) the error message "Spawn is supported only in SMC" is emitted by symbolic engine, which means dynamical processes are not supported by symbolic engine (symbolic simulator and symbolic queries) and it cannot be supported there in principle, because that engine assumes finite state spaces, whereas spawn can create potentially infinite amount of processes. Spawn is supported only in Monte-Carlo simulations which means SMC engine only.

3) Dynamic processes (spawn etc) are supported in SMC queries (verifier) and to my best knowledge it works there. If the verifier does not work for you, then I would like to know the details.

4) unfortunately the current concrete simulator does not implement the dynamic processes (and also dynamical equations) because as a university we have research priorities. It does not mean the development has stopped. We are hiring and I hope to solve this during next year.

Best wishes and happy holidays!

Marius