Skip to content

PRISM parser for POMDPs fails when observables is not the first definition after model header #701

Open
@TheGreatfpmK

Description

@TheGreatfpmK

If I try to parse a POMDP in PRISM format using the "observables ... endobservables" syntax (PRISM documentation), it seems to only work if this definition is the first thing that's defined after the pomdp header.

In the attachment (see below), there are 2 files with the same POMDP defined, the only difference is that the test-fail.prism contains a definition of some formula before the definition of observables. The test-ok.prism is parsed fine and test-fail.prism fails with:

ERROR (SpiritErrorHandler.h:26): Parsing error at 6:5:  expecting "=", here:
                x
            ^

ERROR (storm-cli.cpp:63): An exception caused Storm to terminate. The message of the exception is: WrongFormatException: Parsing error at 6:5:  expecting "=", here:
                x
            ^

PRISM parses both of these without any issues.

pomdps-test.zip

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