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
  • #178

Closed
Open
Opened May 17, 2016 by Alexandre Duret-Lutz@adlOwner

out-of-date example on satmin.html

On https://spot.lrde.epita.fr/satmin.html#sec-2 there the following example:

There are cases where ltl2tgba's tba-det algorithm fails to produce a deterministic automaton. In that case, SAT-based minimization is simply skipped. For instance:

ltl2tgba -D -x sat-minimize "Ga R (F!b & (c U b))" --stats='states=%s, det=%d'
states=5, det=1

outputting a determinitic automaton contradicts the text.

This is a case where tba-det works. I'm not sure what changed and when it started to work, but we need to find another example of syntactic-recurrence that tba-det cannot determinize.

PS: while we are at it, we should try to favor single-quotes over double-quotes in examples so that users do not get any surprise with interactive shells interpreting !.

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#178