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

AssertionError caused by comparison of integer field and aggregate #1251

Closed
treiher opened this issue Nov 8, 2022 · 1 comment
Closed

AssertionError caused by comparison of integer field and aggregate #1251

treiher opened this issue Nov 8, 2022 · 1 comment
Assignees
Labels
bug model Related to model package (e.g., model verification) small Effort of one person-day or less

Comments

@treiher
Copy link
Collaborator

treiher commented Nov 8, 2022

package Test is

   type T is range 1 .. 10 with Size => 16;

   type M is
      message
         F1 : T
            then null
               if F1 = [1, 2];
   end message;

end Test;
Traceback (most recent call last):
  File "/home/devel/Componolit/RecordFlux/rflx/cli.py", line 259, in main
    args.func(args)
  File "/home/devel/Componolit/RecordFlux/rflx/cli.py", line 307, in check
    parse(args.files, args.no_verification, args.workers)
  File "/home/devel/Componolit/RecordFlux/rflx/cli.py", line 368, in parse
    model = parser.create_model()
  File "/home/devel/Componolit/RecordFlux/rflx/specification/parser.py", line 1854, in create_model
    self._evaluate_specification(error, spec_node.spec, spec_node.filename)
  File "/home/devel/Componolit/RecordFlux/rflx/specification/parser.py", line 1981, in _evaluate_specification
    new_type = handlers[t.f_definition.kind_name](
  File "/home/devel/Componolit/RecordFlux/rflx/specification/parser.py", line 1012, in create_message
    return create_proven_message(
  File "/home/devel/Componolit/RecordFlux/rflx/specification/parser.py", line 1603, in create_proven_message
    proven_message = unproven_message.proven(
  File "/home/devel/Componolit/RecordFlux/rflx/model/message.py", line 2191, in proven
    return Message(
  File "/home/devel/Componolit/RecordFlux/rflx/model/message.py", line 873, in __init__
    self.verify()
  File "/home/devel/Componolit/RecordFlux/rflx/model/message.py", line 893, in verify
    self._prove_contradictions()
  File "/home/devel/Componolit/RecordFlux/rflx/model/message.py", line 1747, in _prove_contradictions
    constraints = self.message_constraints() + self.type_constraints(contradiction)
  File "/home/devel/Componolit/RecordFlux/.venv/lib/python3.10/site-packages/icontract/_checkers.py", line 892, in wrapper
    result = func(*args, **kwargs)
  File "/home/devel/Componolit/RecordFlux/rflx/model/message.py", line 429, in type_constraints
    *self._aggregate_constraints(expression),
  File "/home/devel/Componolit/RecordFlux/rflx/model/message.py", line 456, in _aggregate_constraints
    aggregate_constraints.extend(get_constraints(r.right, r.left))
  File "/home/devel/Componolit/RecordFlux/rflx/model/message.py", line 437, in get_constraints
    assert isinstance(comp, mty.Composite)
AssertionError
@treiher treiher added bug model Related to model package (e.g., model verification) small Effort of one person-day or less labels Nov 8, 2022
@treiher treiher added this to Medium in RecordFlux Future via automation Nov 8, 2022
@senier senier removed this from Medium in RecordFlux Future Nov 29, 2022
@senier senier added this to To do in RecordFlux 2023-01-06 via automation Nov 29, 2022
@senier senier added this to To do in RecordFlux 2023-02-24 via automation Jan 3, 2023
@senier senier removed this from To do in RecordFlux 2023-01-06 Jan 3, 2023
@treiher treiher self-assigned this Aug 21, 2023
@treiher
Copy link
Collaborator Author

treiher commented Aug 21, 2023

Fixed in version 0.12.0.

@treiher treiher closed this as completed Aug 21, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug model Related to model package (e.g., model verification) small Effort of one person-day or less
Projects
No open projects
Development

No branches or pull requests

1 participant