title now
body.

environment ID: E
Relations:
  • Path: StringLoc x StringLoc
Initial interpretation must include:

Variables:
  • secON : BOOLE
  • armed : BOOLE
Local actions:
    Sync actions:
    • gotoC: Att
      pre: TRUE
      post: E.armed(e)=TRUE
    • gotoB: Att
      pre: TRUE
      post: E.secON(e)=TRUE
    • off: Att
      pre: E.secON(e)=TRUE
      post: E.secON(e)=FALSE
    • pulse:
      pre: E.armed(e)=TRUE
      post: E.armed(e)=FALSE
    Initial state:
    • secON: TRUE
      armed: FALSE


    agent ID: Att
    Variables:
    • loc : StringLoc
    • destroyed : BOOLE
    Local actions:
    • gotoA:
      pre: Att.loc(self)=init & Path(init,A)
      post: Att.loc(self)=A
    Sync actions:
    • gotoC:
      pre: Att.loc(self)=B & E.secON(e)=FALSE & Path(B,C)
      post: Att.loc(self)=C
    • gotoB:
      pre: Att.loc(self)=A & Path(A,B)
      post: Att.loc(self)=B
    • off:
      pre: Att.loc(self)=A
      post: TRUE
    • pulse: E
      pre: Att.loc(self)=C
      post: Att.destroyed(self)=TRUE
    Individual sync actions:
      Initial state:
      • loc: init
        destroyed: FALSE

      ?


      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