WIP Improved cover analysis output

[Kukovec]

For example, given

--------------------------- MODULE test -------------------------------------

EXTENDS Integers

VARIABLE x,y

Init == x = 1 /\ y = 1

A1 == x' = 1 \/ x' = 2
A2 == x' = 3 \/ x' = 4
B1 == y' = 1 \/ y = 2
B2 == x' = 1 /\ (y' = 3 \/ y' = 4)

Next == 
    \/ A1 /\ B1
    \/ A1 /\ B2
    \/ A2 /\ B1
    \/ A2 /\ B2

=============================================================================

the new output is

test.tla:7:9-7:13   : Init may update x
test.tla:7:18-7:22  : Init may update y
test.tla:9:7-9:12   :   A1 may update x
test.tla:9:17-9:22  :   A1 may update x
test.tla:10:7-10:12 :   A2 may update x
test.tla:10:17-10:22:   A2 may update x
test.tla:11:7-11:12 :   B1 may update y
test.tla:12:18-12:23:   B2 may update y
test.tla:12:28-12:33:   B2 may update y

test.tla:7:9-7:22   : Init always updates: x, y
test.tla:9:7-9:22   :   A1 always updates: x
test.tla:10:7-10:22 :   A2 always updates: x
test.tla:11:7-11:21 :   B1 sometimes does not update: y 	 [WARNING!] 
test.tla:12:7-12:34 :   B2 always updates: y

Closes #298.

[Kukovec]

Side-note, I see some tests are failing because source information for operators is unavailable, this is an indication of an unrelated underlying bug.

[shonfeder]

Side-note, I see some tests are failing because source information for operators is unavailable, this is an indication of an unrelated underlying bug.

I suggest we fix the underling but here, or else in a separate PR that we merge in ahead of this one. We don't want to break the integration tests on the development branch, because it could then hide other regressions that show up later (prior to getting in the proper fix).

[Kukovec]

The reordering of passes to accommodate the new cover analysis (specifically, addressing the incompatibility with inlining, which now deletes operator definitions from the module) should get its own PR, so this one should be put on hold until all bugs arising from the reordering are isolated, as not to get saturated with commits not related to cover analysis.

[shonfeder]

(Marked as WIP so it doesn't show in our daily alerts for stale PRs) :)

[konnov]

What is the status of this PR?

[Kukovec]

What is the status of this PR?

Since other PRs (#343, previously #347) are linked to bugs and are thus more pressing, work on this will resume after #343 closes.

[Kukovec]

#366 removed the need for cover analysis, so I'm scrapping this PR.