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

Closed
Open
Created May 28, 2025 by Pablo Laciana@placianaOwner

STOP button is not working

Hernán Gabriel Gagliardi created an issue 2025-05-20 Is not working when you run synthesis for a large example:

‌

const N = 7 const K = 7

const Amenities = N const Steps = K

range Amenity = 0..(Amenities-1) range Step = 0..(Steps-1)

/*****************************************************************************/

Agency = (agency.request -> Processing), Processing = ( {agency.fail,agency.succ} -> Agency | query[Amenity] -> Processing ).

Service(Sid=0) = ( {agency.succ,agency.fail} -> Service | query[Sid] -> ( unavailable[Sid] -> query.fail[Sid] -> Service | available[Sid] -> steps[Sid][s:Step] -> query.succ[Sid] -> Selection[s] )), Selection[s:Step] = if (s>0) then (select[Sid] -> Selection[s-1]) else Booking, Booking = ( committed[Sid] -> if (Sid==Amenities-1) then Reserve else (query[Sid+1] -> Reserve) | uncommitted[Sid] -> if (Sid==Amenities-1) then Direct else (query[Sid+1] -> Direct) ), Reserve = ( {agency.succ,agency.fail} -> Service | cancel[Sid] -> Service | purchase[Sid] -> purchase.succ[Sid] -> Service ), Direct = ( {agency.succ,agency.fail} -> Service | cancel[Sid] -> Service | purchase[Sid] -> ( purchase.succ[Sid] -> Service | purchase.fail[Sid] -> Service ) ).

ServiceMonitor(Sid=0) = ( query[Sid] -> InQuery | agency.succ -> ERROR | agency.fail -> ServiceMonitor ), InQuery = ( query.succ[Sid] -> QuerySucces | query.fail[Sid] -> QueryFail | agency.succ -> ERROR | agency.fail -> ServiceMonitor ), QuerySucces = ( purchase.succ[Sid] -> Success | purchase.fail[Sid] -> QueryFail | cancel[Sid] -> QueryFail | agency.succ -> ERROR | agency.fail -> ServiceMonitor ), QueryFail = ( agency.succ -> ERROR | agency.fail -> ServiceMonitor ), Success = ( agency.succ -> ServiceMonitor | agency.fail -> ServiceMonitor ).

AgencyMonitor = Disallow[0], Disallow[n:0..1] = ( agency.fail -> ERROR | agency.succ -> AgencyMonitor | query.fail[Amenity] -> Allow | uncommitted[Amenity] -> if (n==0) then Disallow[1] else Allow | when (n==1) purchase.fail[Amenity] -> Allow ), Allow = ( {agency.fail,agency.succ} -> AgencyMonitor | {query.fail[Amenity],uncommitted[Amenity],purchase.fail[Amenity]} -> Allow ).

/*****************************************************************************/

||Plant = ( Agency || AgencyMonitor || forall [a:Amenity] (Service(a) || ServiceMonitor(a)) ).

set Allactions = {agency.request, agency.fail, agency.succ, query[a:Amenity], unavailable[a:Amenity], query.fail[a:Amenity], available[a:Amenity], query.succ[a:Amenity], steps[a:Amenity][s:Step], committed[a:Amenity], uncommitted[a:Amenity], cancel[a:Amenity], purchase[a:Amenity], purchase.succ[a:Amenity], purchase.fail[a:Amenity]}

fluent F = <{agency.succ, agency.fail}, Allactions{agency.succ, agency.fail}> assert A = F

controllerSpec Goal = { controllable = {cancel[Amenity],purchase[Amenity], agency.succ, agency.fail} liveness = {A} } assert Check = ([]<>A)

controller ||MonolithicController = Plant~{Goal}.

Edited May 28, 2025 by Pablo Laciana
Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking