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}.