Skip to content

Add support for both kinds of non-determinism in the JANI translation #108

@matseblenkamp

Description

@matseblenkamp

Currently procs only support demonic choice and coprocs angelic choice, since procs get translated to Emin in JANI and coprocs to Emax. This means there is no possibility to get an upper bound on an infimum or a lower bound on a supremum. Adding support for both angelic and demoic non-determinism independ of proc and coproc would make sense.

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