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 111
    • Issues 111
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge Requests 2
    • Merge Requests 2
  • 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
  • #51

Closed
Open
Opened Jan 15, 2015 by Alexandre Duret-Lutz@adlOwner4 of 7 tasks completed4/7 tasks

fusion-star support

This keep tracks of the support for the [:*i..j] operator. This is currently on branch adl/si-psl.

  • documentation of semantics, parsing, pretty-printing, trivial simplifications, translation
  • update ltl2tgba.html to mention the operator
  • non-trivial simplifications
  • is_syntactic_stutter_invariant() following Def.2 of Dax et al. (ATVA'09)
  • generalize remove_x() following function κ and τ in Dax et al. (ATVA'09) (bug this seems bogus, see comment below)
  • investigate why we need a bidirectional check in our implementation of is_stutter_invariant() using Etessami's rewriting, why Dax et al. (ATVA'09) claim that their τ function (based on the paper of Peled & Wilke) is an overapproximation, and therefore would need only one inclusion check. Is it the case that Etessami's function is also an overapproximation and we are doing to much work or is it the case that Etessami's is not an overapproximation?
  • generalize the syntactic version of is_stutter_invariant() to use stutterize_psl()
To upload designs, you'll need to enable LFS and have admin enable hashed storage. More information
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: spot/spot#51