Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
Spot
Spot
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 117
    • Issues 117
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 1
    • Merge Requests 1
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
  • Spot
  • SpotSpot
  • Issues
  • #388

Closed
Open
Opened May 21, 2019 by Alexandre Duret-Lutz@adlOwner

confusing diagnostic

On Tue, May 21, 2019 at 5:47 PM Victor Khomenko wrote:

Hi Alexandre,

I tried the formula {(a:b) | (a;b)}|->Gc in the online tool, and it correctly tells that it's stutter-sensitive, with

    Accepted word:  a & !b & c; a & !b & c; cycle{b & !c}
    Rejected word:  a & !b; cycle{b & !c}

Then it claims that the words differ only by some stuttering, which is not quite true. I think one should add & c to the first letter of the rejected word.

Regards, Victor.

This is really an issue for spot/spot-web-app> but we should fix it in the explain_stut() function of stutter-inv.ipynb as well. We just need to make sure that each letter of word uses all atomic propositions (the missing ones can be set to positive or negative, it does not matter).

Edited May 21, 2019 by Alexandre Duret-Lutz
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: spot/spot#388