# SPDX-License-Identifier: ISC import syndicate/assertions, syndicate/dataspaces, syndicate/events, syndicate/skeletons import preserves, preserves/records import asyncdispatch, tables, options const N = 100000 const `?_` = init(Discard) `?$` = init(Capture, `?_`) BoxState = RecordClass(label: symbol"BoxState", arity: 1) SetBox = RecordClass(label: symbol"SetBox", arity: 1) proc boot(facet: Facet) = facet.spawn("box") do (facet: Facet): facet.declareField(value, int, 0) discard facet.addEndpoint do (facet: Facet) -> EndpointSpec: # echo "recomputing published BoxState ", facet.fields.value let a = BoxState.init(value.getPreserve) result.assertion = some a discard facet.addDataflow do (facet: Facet): # echo "box dataflow saw new value ", facet.fields.value if value.get == N: facet.stop do (facet: Facet): echo "terminated box root facet" discard facet.addEndpoint do (facet: Facet) -> EndpointSpec: const a = SetBox.init(`?$`) result.analysis = some analyzeAssertion(a) proc cb(facet: Facet; evt: EventKind; vs: seq[Value]) = if evt == messageEvent: facet.scheduleScript do (facet: Facet): value.set(vs[0]) # echo "box updated value ", vs[0] result.analysis.get.callback = facet.wrap cb const o = Observe.init(SetBox.init(`?$`)) result.assertion = some o facet.spawn("client") do (facet: Facet): discard facet.addEndpoint do (facet: Facet) -> EndpointSpec: const a = BoxState.init(`?$`) result.analysis = some analyzeAssertion(a) proc cb(facet: Facet; evt: EventKind; vs: seq[Value]) = if evt == addedEvent: facet.scheduleScript do (facet: Facet): let v = SetBox.init(vs[0].int.succ.toPreserve) # echo "client sending ", v facet.send(v) result.analysis.get.callback = facet.wrap cb const o = Observe.init(BoxState.init(`?$`)) result.assertion = some o discard facet.addEndpoint do (facet: Facet) -> EndpointSpec: const a = BoxState.init(`?_`) result.analysis = some analyzeAssertion(a) proc cb(facet: Facet; evt: EventKind; vs: seq[Value]) = if evt == removedEvent: facet.scheduleScript do (facet: Facet): echo "box gone" result.analysis.get.callback = facet.wrap cb const o = Observe.init(BoxState.init(`?_`)) result.assertion = some o facet.actor.dataspace.ground.addStopHandler do (_: Dataspace): echo "stopping box-and-client" waitFor bootModule("box-and-client", boot)