Revised State and observation valuations

[tquatmann]

Replaces the sparse StateValuations by a new implementation that stores the values as specified by umb.

Example CLI Usage

Note that we still have to add the --buildstateval switch

# create umb file with state valuations
 storm --buildstateval --prism crowds5_5.pm --exportbuild crowds-storm.umb 
# import umb file with state valuations
storm --buildstateval -umb crowds-storm.umb

Observation Valuations

For POMDPs, we can also use the --buildobsval switch to add observation valuations.
This no longer treats observations as strings, but rather as a valuation.

Compatibility

So far, I've manually tested whether we can exchange models with state valuations with prism.

Implementation Details

The core parts are in storm/storage/umb/model/Valuations.h. Reading from and writing to variables works via callbacks. This has the advantage, that we always access the variable value in the most suitable type (Side note: for integer variables, the "right" type (uint64_t vs. int64_t vs. arbitrary precision Integer) is not easy to determine).

storm/storage/sparse/valuations.h serves as a higher-level wrapper that doesn't expose callbacks. It mostly restores the old functionalities of StateValuations.h. Notable changes:

• the old blowUp method is now selectEntities
• hash() now does something properly (it just returned 0 before)
• Iterating over all values is now slightly different. We can either invoke getAllVariables() and then get the value for each variable or we use a callback function via getUmbValuations().readCallback....

[sjunges]

I am somewhat confused that creating state valuations is now done via the umb (sub)library, rather than via what is in sparse. In e.g., the monitor-verifier, this yields very unexpected inclusions.

[sjunges]

Do we never rely on these names coinciding etc. I see how this is a local fix, but I wonder whether it hides problems downstream.

[tquatmann]

For example Prism allows this

observable "s" = s;

Now I wonder if even this would be allowed:

observable "s" = s+x;

I can see that this is problematic. We could also just fail with an error message in the second case, i.e., whenever there is a observable "x" = expr; statement where x is also a used variable identifier and expr is not just the variable expression x.

[tquatmann]

Anything else would require a second expression manager for the "observation valuations" which I'd prefer not to have

[sjunges]

i think this observable "s" = s; is an antipattern... i would not allow it? :-)

[tquatmann]

observable "s" = s; is explicitly mentioned on the PRISM webpage.
I have seen a number of PRISM files with e.g. label "done" = done;, so I get where also allowing this for observable is coming from.
IMO observable "s" = s; is not bad enough to justify breaking compatibility with PRISM.

It also avoids having to mix both syntaxes, which is arguably quite clean

observables s endobservables
observable "parity" = x % 2;

vs.

observable "s" = s;
observable "parity" = x % 2;

[tquatmann]

After internal discussions, we decided to allow the pattern observable "s" = s but not observable "s" = expr for variable s and expr ≠ s (as it's implemented right now)

[sjunges]

Overall looks very good. I dont like that the valuations are in the UMBI folder as noted above and the callbacks are partially a bit hard to read, but not sure how to improve that.

[tquatmann]

I am somewhat confused that creating state valuations is now done via the umb (sub)library, rather than via what is in sparse. In e.g., the monitor-verifier, this yields very unexpected inclusions.

The internal storage should be UMB compliant, which is why the file is currently located there.
I can see that this is currently weird when we just need a data structure for valuations without an immediate intention to export it. My suggestion is to

• mkdir storm/storage/valuations and move relevant files there.
• This includes storm/storage/umb/model/Valuations.[h|cpp] (rename to ValuationsStorage), storm/storage/umb/utility/ValuationDescriptionBuilder.[h|cpp], and storm/storage/umb/model/ValuationDescription.[h|cpp].
• Add a corresponding comment in those files that need to be UMB compliant
• Rename storm::storage::sparse::StateValuations::getUmbValuations() to getStorage()

There will still be some transitive(!) umb includes, but I guess that's ok

[tquatmann]

the callbacks are partially a bit hard to read, but not sure how to improve that.

Me neither. They are quite flexible and efficient but that also makes them awkward sometimes. I'm open for feedback

[sjunges]

Thanks for the fixes and clarifications. LGTM. Shall we merge or should I first create updated bindings?

[tquatmann]

I made two more commits following the discussions above:

• one commit creates src/storm/storage/valuations/, moves things there (in particular of the umb scope), and adapted namespaces and function names accordingly
• one that rejects Prism Programs in one of the two cases:
  • There is a variable or constant named _OutOfBoundsBit and --build-out-of-bounds-state --buildstateval is set
  • There is a label observable "s" = <expr>; and s is already a variable and the expression <expr> is not equal to s.

[tquatmann]

Shall we merge or should I first create updated bindings?

imo, we can delay merging this a bit to reduce the time in which stormpy is broken with storm's main.

Feel free to merge this at your convenience :)

And thanks for the great feedback!