DEFINITIONS
  // DEFINITIONS for VisB visualisation
  VISB_JSON_FILE == "";
  VISB_SVG_BOX == rec(height∈800, width∈400);
  "LibraryStrings.def";

  StateNr == [z0,z1,z2,ze]⁻¹;
  HEIGHT == 13; WID==HEIGHT;
  OFF == 2;
  VISB_SVG_OBJECTS_State ==
   {t,s • t∈TIME ∧ s∈States |
     rec( svg_class:"rect",
         `id`: ("state",t,s),
          height:HEIGHT, width:WID,
          stroke:"black",
          x:(WID+OFF)*(t)+5,
          y:StateNr(s)*(HEIGHT+OFF)+20,
          fill: IF state(t,s) = TRUE THEN "purple" ELSE "white" END
        )};
  VISB_SVG_OBJECTS_Head ==
   {t,p • t∈TIME ∧ p∈POS |
     rec( svg_class:"rect",
         `id`: ("head",t,p),
          height:HEIGHT, width:WID,
          stroke:"black",
          x:(WID+OFF)*(t)+5,
          y:(p+pn)*(HEIGHT+OFF)+20+4*(HEIGHT+OFF)+40,
          fill: IF head(t,p) = TRUE THEN "purple" ELSE "white" END) };
  VISB_SVG_OBJECTS_Tape ==
   {t,p • t∈TIME ∧ p∈POS |
     rec( svg_class:"rect",
         `id`: ("tape",t,p),
          height:HEIGHT, width:WID,
          stroke:"black",
          x:(WID+OFF)*(t)+5,
          y:(p+pn)*(HEIGHT+OFF)+60+(4+1+2*pn)*(HEIGHT+OFF)+40,
          fill: IF card({a|a:Alphabet & tape(t,p,a)=TRUE})>1 THEN "gray"
                ELSIF tape(t,p,`◻︎`) = TRUE THEN "white"
                ELSIF tape(t,p,I) = TRUE THEN  "green"
                ELSE "red" END) };

 VISB_SVG_OBJECTS3_InfoText ==
     rec( svg_class:"text",
         `id`: "infotext2",
          text: "SAT Variables",
          x:10,
          y:20);
 VISB_SVG_HOVERS_state ==
   {t,p • t∈TIME ∧ p∈States |
      rec(`trigger_id`: ("state",t,p),
          `id`: "infotext2",
           text: "state "^TO_STRING(t)^","^TO_STRING(p)
         )
    };
 VISB_SVG_HOVERS_head ==
   {t,p • t∈TIME ∧ p∈POS |
      rec(`trigger_id`: ("head",t,p),
          `id`: "infotext2",
           text: "head "^TO_STRING(t)^","^TO_STRING(p)
         )
    };
 VISB_SVG_HOVERS_tape ==
   {t,p • t∈TIME ∧ p∈POS |
      rec(`trigger_id`: ("tape",t,p),
          `id`: "infotext2",
           text: "tape "^TO_STRING(t)^","^TO_STRING(p)^",{O,I,◻︎}"
         )
    };
