Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
M MTSA
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 68
    • Issues 68
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Operations
    • Operations
    • Metrics
    • Incidents
    • Environments
  • Packages & Registries
    • Packages & Registries
    • Package Registry
  • Analytics
    • Analytics
    • CI/CD
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • lafhis
  • MTSA
  • Issues
  • #82

Closed
Open
Created Jun 04, 2025 by Sebastian Uchitel@suchitelOwner

LTL Model checking error

If you check OBS2 against TEST you get a counterexample that does not violate the property

// MUSEO

CONTROL = (open -> ticket->entry-> close -> exit -> CONTROL).

||Test = CONTROL.

assert OBS2 = [](close -> (!(exit) U open))

Trace to terminal set of states: open ticket entry close exit open ticket entry close Cycle in terminal set: exit open ticket entry close

The right output is

open ticket entry close exit


Edited Jun 04, 2025 by Sebastian Uchitel
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking