Project

General

Profile

Bug #1098

Semantics of Idle Actions different in Simulator and Model Checker

Added by Anonymous almost 8 years ago. Updated almost 8 years ago.

Status:
Closed
Priority:
High
Assignee:
-
Category:
-
Start date:
12/19/2012
Due date:
% Done:

100%

Estimated time:

Description

This inconsistency appears for example during test case generation. A deterministic automaton with idle actions is non-deterministic in the model checking model because idle actions have guards true. While the simulator never takes the idel action if any transition can be fired, the model checker might also take the idle action, although a transition is enabled.

This has consequences e.g., in the test case generation, as simulator and model checker return different values, although the automaton is deterministic.

AF3-Project.af3_20 (18.1 KB) AF3-Project.af3_20 Anonymous, 12/19/2012 04:24 PM
TestCase.PNG (8.49 KB) TestCase.PNG Anonymous, 01/24/2013 11:29 AM

History

#1 Updated by Anonymous almost 8 years ago

  • Target version set to Phoenix 2.3 RC2 (Major Bugs)

can you please create a small test model where this problem occurs?

#2 Updated by Anonymous almost 8 years ago

#3 Updated by Anonymous almost 8 years ago

  • Target version set to Phoenix 2.3 RC2 (Major Bugs)

#4 Updated by Anonymous almost 8 years ago

Daniel Ratiu wrote:

can you please create a small test model where this problem occurs?

I attached a small example. The automaton is deterministic. Both transitions have guard true and should be enabled every time. However, when creating a transition coverage test suite, the idle action of the initial state is taken by the model checker.

Maybe this is not so unintuitive since this is actually a transition in the model. However, this transition should never be enabled. In the simulator this is the case. In the model checker it is not.

BTW: If you perform an "Update Test Suite" action on the test suite, the model checking value is removed from test suite as this action only triggers the simulator and not the model chekcer again.

#5 Updated by Anonymous almost 8 years ago

  • Assignee changed from Anonymous to Anonymous

#6 Updated by Anonymous almost 8 years ago

  • Status changed from New to Resolved
  • Assignee changed from Anonymous to Anonymous
  • % Done changed from 0 to 90

I have modified the coverage analyzer and fixed this bug. Please test the nightly build. The update test suite action only calls the simulator because the original parameters for generation of the test cases are not available. This will be improved in the next release.

#7 Updated by Anonymous almost 8 years ago

  • File TestCase.PNG TestCase.PNG added
  • Status changed from Resolved to In Progress
  • Assignee changed from Anonymous to Anonymous

Please consider the sample model that I have attached in comment #2. It still generates strange (wrong) test cases. Generating a transition coverage test leads to an impossible test case (see screenshot).

#8 Updated by Anonymous almost 8 years ago

  • Assignee changed from Anonymous to Anonymous
  • Priority changed from Normal to High

I just realized that I have tested the model with renamed state machine, which produces a correct result. For the original model you attached, the result is always wrong. This relates to a fundamental bug in the kernel and not located in testing plugin. Now I modified the kernel code and think the bug is away. Please confirm whether it is real fixed. Thanks.

#9 Updated by Anonymous almost 8 years ago

  • Status changed from In Progress to Closed
  • Assignee deleted (Anonymous)
  • % Done changed from 90 to 100

Works now for the sample input. However, now test cannot be generated for Formal Specifications in MIRA. See Bug #1203 .

Also available in: Atom PDF