kind2-mc/kind2 — pull request #109 by kevinclancy (2014-08-08 19:49:57+00:00)
Title: Separate counterexamples for separate properties

This modification generates seperate cones of influence for each property. It then displays a separate counterexample for each property, which it generates by culling the counterexample model with respect to the cone of influence of the property in question.

Added a new parameter "start_at_init" to the tree path printing functions in the lustrePath module. This allows us to control whether the first terms of the model's streams are interpreted as values at the initial instance. This may be set to false to display models that begin after the initial instance (in which case expr_step is used to reconstruct the first term rather than expr_init).

Also made a few other minor modifications. I removed the non-stateless-variable-reconstructing path printing functions because I do not think there's any point to having them. If, for debugging purposes, we need to view paths before stateless variables have been reconstructed, we could accomplish this by modifying the printing functions to not reconstruct stateless variables.