Skip to content

Expansion of modal expressions is incorrect #5

@joseproenca

Description

@joseproenca

In Reo, when verifying dupl; fifo*(lossy;out), the modal logic:

  • <out> true

Is expanded to:

  • <(dupl_1i1|out_3o1)> true

But it should be expanded to:

  • <dupl_1i1|dupl_1o1_fifo_2i1|dupl_1o2_lossy_3i1|lossy_3o1_out_4i1|out_4o1

Hence the formula wrongly evaluates to false.

Metadata

Metadata

Assignees

Labels

Type

No type
No fields configured for issues without a type.

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions