body.

environment ID: E

Relations:

Initial interpretation must include:

Variables:

state : State

Local actions:

Sync actions:

allow_n:
pre: E.state(env)=PGreen
post: E.state(env)=NGreen
allow_p:
pre: E.state(env)=NGreen
post: E.state(env)=PGreen
p_enter: PT
pre: E.state(env)=PGreen
post: E.state(env)=Red
n_enter: NT
pre: E.state(env)=NGreen
post: E.state(env)=Red
p_exit: PT
pre: E.state(env)=Red
post: E.state(env)=PGreen
n_exit: NT
pre: E.state(env)=Red
post: E.state(env)=NGreen

Initial state:

state: PGreen

agent ID: PT

Variables:

state : State

Local actions:

p_approach:
pre: PT.state(self)=Away
post: PT.state(self)=Waiting

Sync actions:

allow_p: E
pre: PT.state(self)=Forbidden
post: PT.state(self)=Away
allow_n: E
pre: PT.state(self)=Away
post: PT.state(self)=Forbidden

Individual sync actions:

p_enter:
pre: PT.state(self)=Waiting
post: PT.state(self)=Tunnel
p_exit:
pre: PT.state(self)=Tunnel
post: PT.state(self)=Away

Initial state:

state: Waiting

agent ID: NT

Variables:

state : State

Local actions:

n_approach:
pre: NT.state(self)=Away
post: NT.state(self)=Waiting

Sync actions:

allow_n: E
pre: NT.state(self)=Forbidden
post: NT.state(self)=Away
allow_p: E
pre: NT.state(self)=Away | NT.state(self)=Wait
post: NT.state(self)=Forbidden

Individual sync actions:

n_enter:
pre: NT.state(self)=Waiting
post: NT.state(self)=Tunnel
n_exit:
pre: NT.state(self)=Tunnel
post: NT.state(self)=Away

Initial state:

state: Forbidden

main controls

more options

witness of unsafety

Work in progress.

Conclusions

Work in progress.

Safe Swarms Club

better be safe than sorry

SAFE Base

SAFE Base Fresh Start

SAFE For All

SAFE For All

SAFE Data

SAFE Data