Skip to content

Unexpected behavior when sampling distributions as part of larger assignments #4

@LunDev

Description

@LunDev

I've explored this tool over the past few months, and this one minor issue was the source of a lot of confusion for me.

Consider these two Prob-solvable loop programs:

a = 0
while true:
    b = RV(uniform, 0, 2)
    a = a + b

and

a = 0
while true:
    a = a + RV(uniform, 0, 2)

Computing the moment-based invariants of these programs for the first-order moments (python run.py --benchmarks inputtest --goal 1) leads to
E[a] = n as expected for the first program and
E[a] = 1 for the second program - which doesn't make much sense.

This behavior greatly confused me until someone pointed out to me that the grammar specification provided in Mora - Automatic Generation of Moment-Based Invariants doesn't allow sampling of random distributions as part of larger assignments. While the short language specification in the readme is technically correct as it doesn't claim that this would be supported, some parts can quite easily be misunderstood.

[...] In the variable updates as well as the initial assignments, random variables can be used.
[...]
Random variables:

  • format: var = RV(distribution, parameter1, [parameter2, ...])

If one misses the prefix var =, one might easily think that random sampling is permissible in variable update assignments, when it actually only is allowed as separate statements.

I initially got this wrong idea by trying to implement one of the examples in Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops, which contains such update assignments like x := x + f * rand(1-d, 1+d).

Mora just quietly ignores this mistake in syntax and treats these invalid assignments as if they would only consist of the random sampling. It would be great if it could either complain with a syntax error, correctly handle such composite statements or this behavior at least got explicitly stated in the documentation in order to save new users like me. Thank you!

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions