Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • Spot Spot
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 133
    • Issues 133
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Environments
    • Releases
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • SpotSpot
  • SpotSpot
  • Issues
  • #46
Closed
Open
Issue created Jan 04, 2015 by Alexandre Duret-Lutz@adlOwner

add option to output neverclaims in spin 6.2.4's format

In 2013 Spin 6.2.4 changed the way it outputs neverclaim. The current parser can read both styles, but so far we only output the old style.

Compare:

% spin-6.2.2 -f '<>a || []b'
never  {    /* <>a || []b */
T0_init:
        if
        :: ((b)) -> goto accept_S2
        :: ((a)) -> goto accept_all
        :: (1) -> goto T0_S5
        fi;
accept_S2:
        if
        :: ((b)) -> goto accept_S2
        fi;
T0_S5:
        if
        :: ((a)) -> goto accept_all
        :: (1) -> goto T0_S5
        fi;
accept_all:
        skip
}
% spin-6.4.3 -f '<>a || []b'
never  {    /* <>a || []b */
T0_init:
        do
        :: ((b)) -> goto accept_S2
        :: atomic { ((a)) -> assert(!((a))) }
        :: (1) -> goto T0_S5
        od;
accept_S2:
        do
        :: ((b)) -> goto accept_S2
        od;
T0_S5:
        do
        :: atomic { ((a)) -> assert(!((a))) }
        :: (1) -> goto T0_S5
        od;
accept_all:
        skip
}

So ifs have been changed into dos, and transitions to accept_all: have been replaced by these atomic/assert combinations. IIRC Holzmann said this improves counterexamples. I do not know if the accept_all: state is necessary in the new format.

Assignee
Assign to
Time tracking