This issue tracker is closed. Please visit UPPAAL issue tracker at Github instead.

Bug 544

Summary: support for clock and random initialisers (initializers)
Product: UPPAAL Reporter: Marius Mikučionis <marius>
Component: EngineAssignee: Marius Mikučionis <marius>
Status: ASSIGNED ---    
Severity: enhancement    
Priority: P5    
Version: 4.1.13   
Hardware: All   
OS: All   
Architecture:
Attachments: non-zero initializer break invariant in initial location

Description Marius Mikučionis 2013-01-17 11:22:48 CET 
There are two problems:

1) default clock initialiser (0) obscures SMC models by having value zero which does not always make sense, it also obscures query results (see bug 543)

2) stochastic and dynamical systems may have random initial states, it would be convenient to define it with initialiser.
Comment 1 Marius Mikučionis 2017-04-06 13:41:05 CEST 
Created attachment 309 [details]
non-zero initializer break invariant in initial location