Skip to content

GitLab

  • Menu
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 132
    • Issues 132
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 2
    • Merge requests 2
  • 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
  • Spot
  • SpotSpot
  • Issues
  • #405

Closed
Open
Created May 06, 2020 by Alexandre Duret-Lutz@adlOwner

suboptimal behaviour of simplify_acceptance()

Consider the automaton

HOA: v1
States: 2
Start: 0
AP: 2 "p0" "p1"
Acceptance: 5 (Fin(0) & Fin(3)) & (Fin(1)|Fin(2)|Fin(4))
properties: trans-labels explicit-labels trans-acc
--BODY--
State: 0
[!0&!1] 0 {0 1 4}
[0&1] 1 {0 2 3}
State: 1
[0&1] 0 {0 2 3}
[0&1] 1 {1}
--END--

I'm not sure what is going on with the following simplifications.

foo

Since colors 2 & 3 are identical, I would expect the original condition to be reduced to (Fin(0) & Fin(2)) & (Fin(1)|Fin(2)|Fin(4)) then unit-propagation should reduce this to Fin(0)&Fin(2) and fusing of Fin-conjuncts should simplify this to Fin(1) while adjusting the automaton.

It's not clear to me what rules allow to simplify (Fin(0) & Fin(3)) & (Fin(1)|Fin(2)|Fin(4)) to (Fin(0) & (Fin(1)|Fin(2)|Fin(4)). It this because 3 and 2 are complementary? (Would that be a valid reduction?)

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking