JSON output lacks the second predicate for 'a NFby a' invariants

[GoogleCodeExporter]

When outputting a JSON object representation of a Perfume model, extra NFby 
invariants are added. Specifically, it seems like it behaves in this way: for 
any predicate *a* for which there exists one or more [[*a* NFby *anything*]] 
invariants, an extra [[*a* NFby]] is added (the second predicate is actually 
blank in the JSON).

Original issue reported on code.google.com by tonyohm...@gmail.com on 26 May 2014 at 1:26

[GoogleCodeExporter]

The JSON doesn't actually contain extra invariants but instead is 
misrepresenting invariants with only one unique predicate (NFby is the only 
possible invariant where this is possible, e.g., "a NFby a"). This is because 
BinaryInvariant.getPredicates() returns a set, so in the case of "a NFby a", 
the set will only contain one "a" because the predicates are not unique.

If the above is undesirable, we could make getPredicates() return a set. This 
will involve many small changes that overflow into the KTails code 
(KTailInvariant and BinaryInvariant implement the same interface that defines 
getPredicates() to return a set). If we don't mind the above behavior, we can 
add a trivial workaround in JsonExporter.

Original comment by tonyohm...@gmail.com on 28 May 2014 at 10:31

• Changed title: JSON output lacks the second predicate for 'a NFby a' invariants
• Changed state: Started

[GoogleCodeExporter]

Correction:
If the above is undesirable, we could make getPredicates() return a *list*. 
[...]

Original comment by tonyohm...@gmail.com on 28 May 2014 at 10:35

[GoogleCodeExporter]

We chose to implement a workaround in JsonExporter. Merged fix into default 
with revision 32f9d232d8ea.

Original comment by tonyohm...@gmail.com on 30 May 2014 at 12:02

• Changed state: Fixed