On lions, impala, and bigraphs: modelling interactions in physical/virtual spaces

Steve Benford, Muffy Calder, Tom Rodden, Michele Sevegnani

Supplementary material

This page presents the source code for the two bigraphical models used in the experiments presented in the paper and the artifacts generated during the runs.

Restricted model

This model assumes a fixed number of players (4) in the initial state, and restricts the admissible GPS updates to the 5 movements observed in the trace. The complete specification of the model in the BigraphER language is reported below. Otherwise, download [savannah.big]. Highlighted definitions are active; this means the corresponding graphical forms can be displayed by clicking on them.

###### Controls

ctrl Locale = 1;
ctrl Localeattack = 1;
ctrl Aura = 1;
fun ctrl Area(i) = 1;

atomic ctrl Lion = 1;
atomic ctrl Lionattack = 2;
atomic ctrl Liongroup = 2;

atomic ctrl Impala = 1;
atomic ctrl Impalaseen = 2;
atomic ctrl Impalaheld = 2;

atomic ctrl Field = 0;

atomic fun ctrl GPS(i) = 1;

atomic ctrl Child = 1;
atomic ctrl Childattack = 1;
atomic ctrl Childgroup = 1;

###### Rules of the game

big attack_lhs =
  Child{a} || Locale{m}.(Lion{a} | Impala{b} | id(1));
big attack_rhs =
  /l (Childattack{a} || Localeattack{m}.(Lionattack{a,l} | Impalaseen{b,l} | id(1)));

react attack =
  attack_lhs -> attack_rhs;

react timeout1 =
  attack_rhs -> attack_lhs;

react join1 =
  /l (Child{a} || Childattack{a'} || (Lion{a} | Lionattack{a',l} | Impalaseen{b,l}))
  ->
  /l (Childgroup{a} || Childgroup{a'} || (Liongroup{a,l} | Liongroup{a',l} | Impalaheld{b,l}));

react timeout2 =
  /l (Childgroup{a} || Childgroup{a'} 
      || Localeattack{m}.(Liongroup{a,l} | Liongroup{a',l} | Impalaheld{b,l} | id(1)))
  ->
  Child{a} || Child{a'} || Locale{m}.(Lion{a} | Lion{a'} | Impala{b} | id(1));
  
react join2 =
  /l (Child{a} ||  (Lion{a} | Liongroup{a',l} | Liongroup{a'',l} | Impalaheld{b,l}))
  ->
  /l (Childgroup{a}
      || (Liongroup{a,l} | Liongroup{a',l} | Liongroup{a'',l} | Impalaheld{b,l}));

fun react kill(i) =
  /b/l (Childgroup{a} || Childgroup{a'} || Childgroup{a''}
        || Localeattack{m}.(Liongroup{a,l} | Liongroup{a',l} | Liongroup{a'',l}
                            | Impalaheld{b,l} | id(1))
        || GPS(i){b})      
  ->
  Child{a} || Child{a'} || Child{a''} 
  || Locale{m}.(Lion{a} | Lion{a'} | Lion{a''} | id(1))
  || 1;      

###### Rules for GPS update
       
# Positions p,p' in area a       
fun react mov1(a,p,p') =
  /m (Area(a){m}.(GPS(p){a} | id(1)) || Locale{m}.(Lion{a} | id(1)))
  ->
  /m (Area(a){m}.(GPS(p'){a} | id(1)) || Locale{m}.(Lion{a} | id(1)));

# Position p in area a, position p' in area a'       
fun react mov2(a,a',p,p') =
  /m/m' ((Area(a){m}.(GPS(p){a} | id(1)) | Area(a'){m'})
         || (Locale{m}.(Lion{a} | id(1)) | Locale{m'}))
  ->
  /m/m' ((Area(a){m} | Area(a'){m'}.(GPS(p'){a} | id(1))) 
         || (Locale{m} | Locale{m'}.(Lion{a} | id(1))));

###### Rules for the human perspective

big children = id(1) || Child{a} || Child{a'} || id(1);       
big auras = (Aura{a} | Aura{a'}) || id(2,{a,a'});
big phi = ([{0}, {0,2}, {1,3}, {1}], 4);     
big psi = ([{0}, {0,1,2}, {0,1,3}, {1}], 4);

react aura_join =
  share children by phi in auras 
  ->
  share children by psi in auras;

react aura_disjoin =
  share children by psi in auras 
  ->
  share children by phi in auras;

###### Initial configuration: three girls, a boy, and an impala problem     
big girls =
  share (Child{g} || Child{g'} || Child{g''})
  by ([{0,1,2}, {0,1,2}, {0,1,2}], 3) 
  in (Aura{g} | Aura{g'} | Aura{g''} || id{g, g',g''});     
big boy = Aura{b}.Child{b};       
big field =
  /b/g/g'/g''/i/m/m'/m''
    ((Field | girls | boy)
     || (Locale{m}.(Lion{g} | Impala{i})
         | Locale{m'}.(Lion{g'} | Lion{g''})
         | Locale{m''}.(Lion{b}))
     || (Area(0){m}.(GPS(1){g} | GPS(0){i})
         | Area(1){m'}.(GPS(2){g'} | GPS(3){g''})
         | Area(2){m''}.(GPS(4){b})));

###### Bigraphical reactive system
     
brs
  init field;
  # GPS events only for the example trace     
  rules = [
    { attack, timeout1, join1, timeout2, join2, kill(0),
      mov2(1, 0, 2, 5), mov2(1, 0, 3, 6),  mov2(0, 1, 5, 7),
      mov2(2, 0, 4, 8),  mov2(0, 2, 8, 9) }
  ];
endbrs

The full transition system is displaced below. It has 107 states and 252 transitions. It can be generated by running the following command:

bigrapher savannah.big -svg ts.svg

Red nodes indicate the “problem” trace observed during the user trials:

0 → 3 → 7 → 18 → 38 → 63 → 82 → 97 → 103 → 106

Click on a node to display the corresponding bigraph. Click on to go back to the transition system.

Complete model

In this model, all restrictions on GPS updates are lifted. The definitions of controls and reaction rules are the same as in the restricted model. The only changes are in the definition of the BRS. These are reported in the snippet below. Download [savannah-general.big] for the full model.

###### Bigraphical reactive system

brs
  # Area 0
  int p0, p0' = {0, 1, 5, 6, 8};
  # Area 1
  int p1, p1' = {2, 3, 7, 10, 11};
  # Area 2
  int p2, p2' = {4, 9};

  # Initial configuration
  init field;
  
  # GPS events only for the example trace     
  rules = [
    { attack, timeout1, join1, timeout2, join2, kill(0),
      # Update within the same area  
      mov1(0, p0, p0'), mov1(1, p1, p1'), mov1(2, p2, p2'),
      # Updates 0 -> 1
      mov2(0, 1, p0, p1),
      # Updates 0 -> 2
      mov2(0, 2, p0, p2),
      # Updates 1 -> 0
      mov2(1, 0, p1, p0),
      # Updates 1 -> 2
      mov2(1, 2, p1, p2),
      # Updates 2 -> 0
      mov2(2, 0, p2, p0),
      # Updates 2 -> 1
      mov2(2, 1, p2, p1) }
  ];
endbrs

The computed transition system has 20666 states and 486586 transitions.