Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Bugbox when using 'Reset on a sequence while running without optimization #946

Closed
jklmnn opened this issue Mar 2, 2022 · 0 comments · Fixed by #947
Closed

Bugbox when using 'Reset on a sequence while running without optimization #946

jklmnn opened this issue Mar 2, 2022 · 0 comments · Fixed by #947
Assignees
Labels

Comments

@jklmnn
Copy link
Member

jklmnn commented Mar 2, 2022

When 'Reset is used on a sequence as in the following example:

package Test is

   type U8 is range 0 .. 2 ** 8 - 1 with
      Size => 8;

   type Entr is
      message
         A : U8;
      end message;

   type Entries is sequence of Entr;

   generic
   session Session with
      Initial => Init,
      Final => End_Session
   is
      Entrs : Entries;
   begin
      state Init
      is
      begin
         Entrs'Reset;
      transition
         goto End_Session
      end Init;
      state End_Session is null state;
   end Session;

end Test;

A bugbox is generated if rflx generate is called without optimization:

------------------------------ RecordFlux Bug ------------------------------
RecordFlux 0.6.0-pre
RecordFlux-parser 0.10.0
attrs 21.4.0
icontract 2.6.1
pydantic 1.9.0
pydotplus 2.0.2
ruamel.yaml 0.17.21
z3-solver 4.8.14.0

Optimized: False

Command: /.../RecordFlux/venv/bin/rflx generate test.rflx -d out

Traceback (most recent call last):
  File "/.../RecordFlux/rflx/cli.py", line 201, in main
    args.func(args)
  File "/.../RecordFlux/rflx/cli.py", line 259, in generate
    generator = Generator(
  File "/.../RecordFlux/rflx/generator/generator.py", line 175, in __init__
    self.__generate(model, integration)
  File "/.../RecordFlux/rflx/generator/generator.py", line 250, in __generate
    self.__create_session(s, integration)
  File "/.../RecordFlux/rflx/generator/generator.py", line 261, in __create_session
    session_generator = SessionGenerator(
  File "/.../RecordFlux/rflx/generator/session.py", line 218, in __init__
    self._create()
  File "/.../RecordFlux/rflx/generator/session.py", line 248, in _create
    state_machine = self._create_state_machine()
  File "/.../RecordFlux/rflx/generator/session.py", line 355, in _create_state_machine
    unit += self._create_states(self._session, is_global)
  File "/.../RecordFlux/rflx/generator/session.py", line 729, in _create_states
    actions = [
  File "/.../RecordFlux/rflx/generator/session.py", line 732, in <listcomp>
    for s in self._state_action(
  File "/.../RecordFlux/rflx/generator/session.py", line 1778, in _state_action
    result = self._reset(action, is_global)
  File "/.../RecordFlux/rflx/generator/session.py", line 2957, in _reset
    assert isinstance(reset.type_, rty.Message)
AssertionError

----------------------------------------------------------------------------
@jklmnn jklmnn added the bug label Mar 2, 2022
@jklmnn jklmnn added this to To do in RecordFlux 0.6 via automation Mar 2, 2022
@treiher treiher self-assigned this Mar 2, 2022
@treiher treiher moved this from To do to Implementation in RecordFlux 0.6 Mar 2, 2022
RecordFlux 0.6 automation moved this from Implementation to Done Mar 3, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
No open projects
Development

Successfully merging a pull request may close this issue.

2 participants