search

UPPAALModelChecker / UPPAAL-Meta

This is the offcial meta repo for issue reporting, feature request and public roadmap for the development of UPPAAL.
http://www.uppaal.org
1 stars 0 forks source link

Clock variables not initialized to zero in Simulator #58

Closed LauraPanizo closed 2 years ago

LauraPanizo commented 3 years ago

Describe the bug In the semantics of TA described in [1], clock variables are set to zero in the initial state. However, we have found two simple examples that show how the simulator does not follow this initialization.

[1] https://www.uppaal.com/uppaal-tutorial.pdf

To Reproduce Steps to reproduce the behavior: We provide two models of that show the bug. First model (transition with guard)

  1. Open the model.
  2. Click on Simulator
  3. See a loop-transition from the initial state that is enabled because clock x can be >20.However, initial state invariant is x<=10.

Second model (transition without guard)

  1. Open the model.
  2. Click on Simulator
  3. See a deadlock because clock x can be >10 initially.

Expected behavior In the first model, the simulator should not enable the transition, and only deadlock behavior is simulated. In the second model, the deadlock behavior should not appear. In fact, when the second model is verified against not deadlock property (A [] ! deadlock) the property is satisfied.

Version(s) of UPPAAL tested 4.1.24

Screenshots First model error:

first_model

Second model error:

second_model

Desktop (please complete the following information):

Additional context Add any other context about the problem here.

mikucionisaau commented 2 years ago

Fixed in 4.1.26, also Stratego 8 image