RunSmvProcessor to search variableStore in correct environment

[BLuedtke]

Closes #3

Recap: Counterexamples from verification with nuXmv are missing inputs (for starter details see linked issue).

In Class CompilationContext (package de.cau.cs.kieler.kicool.compilation), the calling of processors to achieve e.g. verification with nuXmv is performed. The processors are called one after the other (see the loops in method @ L225). They return the (compilation-) environment with the changes they made (environmentPrime = processor.compileEntry(environmentPrime)). The changes to the environment made by the first processor are thus available to the second processor, and so on. Meanwhile, there is also a member "startEnvironment" in the CompilationContext class. This captures the environment before the processors are run (with some exceptions for initialization). Changes to the environment made by processors are usually not saved to this startEnvironment.
Judging by the name "startEnvironment", this is the expected behavior: Said environment should preserve the state of the environment when we started compilation.

Now, when starting verification processors for nuXmv verification, we start with a roughly initialized, but rather sparse environment based on startEnvironment. One of the early processors causes the addition of a "VariableStore" to the working environment, which is passed on to the next processor, and so on. As mentioned earlier, this does not change the startEnvironment, just the local environment that is passed on.
This continues until we arrive at the last processor. This processor is called is "RunNuxmvProcessor", which is essentially just a small addition to "RunSmvProcessor". Here, the task is to both run the nuXmv process, and also interpret its outputs. This concerns the generation of counterexample kTraces: For analyzing the counterexample, the processor relies on the variableStore of the environment to decide whether a variable needs to be put into the trace or not (see method getKTrace in class VerificationPropertyCounterexample). Input and output variables do need to be added, internal vars do not need to be.

The problem is that RunSmvProcessor is searching for the variableStore in the startEnvironment when analyzing the results, and not in environment. See line 178 in Class RunSmvProcessor in package de.cau.cs.kieler.verification.processors.nuxmv in the verification plugin. The startEnvironment does not contain the variable store, an empty store is thus returned. As the variableStore is empty, all variables are interpreted as internal, and none are added to the KTrace.

Proposed fix in this pull request:

Change line 178 in Class RunSmvProcessor in package de.cau.cs.kieler.verification.processors.nuxmv in the verification plugin from:

val store = VariableStore.get(compilationContext.startEnvironment)

To

val store = VariableStore.get(environment)

Additionally, in the if-guard on line 178, I've added a check to ensure environment is not null (... && environment !== null).

I tested verification with different models (both passing and not passing invariants and LTLs). Behavior for passing properties stays the same. For failing properties with a counterexample present in the nuXmv log, the counterexample (ktrace) now contains the appropriate variables. In the simulation mode, I could successfully load such a counterexample trace and execute/simulate it as expected.

In the future, the same change might be required for the RunSpinProcessor in the same plugin, which also tries to retrieve the variableStore from the startEnvironment ((Line 146)[https://github.com/kieler/semantics/blob/master/plugins/de.cau.cs.kieler.verification/src/de/cau/cs/kieler/verification/processors/spin/RunSpinProcessor.xtend#L146] in that class).
However, I neither have SPIN configured nor do I have appropriate models for testing SPIN, so I would not be able to test any changes easily. Therefore, I propose to add just a TODO comment at line 146 to mark it for later fixing.

[BLuedtke]

Correction: I'll add the same fix for SPIN and test it. Making that another pull request would just be overhead.

[BLuedtke]

Okay, tested it with the same models - same problem and same fix works for SPIN.

[a-sr]

Nice PR. Thanks!