Skip to content

Action Coverage shows "never enabled" in #model_check report for actions with nonzero generated/distinct successors #9

@Erchiusx

Description

@Erchiusx

Problem

Action Coverage shows "never enabled" for actions with nonzero generated/distinct successors

Reproduction

Use the Autobahn model in:

https://github.com/Erchiusx/veil-dag-rider/blob/veil-2.0-preview/Autobahn-effective-failure.lean

Run the compiled Veil model checker on this file with #model_check.

Observe the Action Coverage widget: several actions are reported as "never enabled" even though the table shows nonzero Generated and Distinct counts for those actions.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions