-- Version 1
-- simple FSM that cycles through the 4 seasons
-- contains only one process
MODULE Year
VAR
  season : {spring, summer, fall, winter};
ASSIGN
  init(season) := spring;
  next(season) := 
    case
      season=spring : summer;
      season=summer : fall;
      season=fall : winter;
      season=winter : spring;
    esac;

MODULE main
VAR 
  y : Year;

-- Spring is always immediatedly followed by summer
-- true
SPEC 
  AG y.season=spring -> AX y.season=summer

-- It's not always winter
-- true
SPEC 
  !AG y.season=winter

-- Winter is always eventually followed by summer
-- true
SPEC
  AG y.season=winter -> AF y.season=summer

-- It's spring infinitely often
-- true
SPEC 
  AG AF y.season=spring

------------------------------------------------------------
-- Version 2
-- contains two processes moving synchronously
-- the first one cycles through the seasons in english
-- the second cycles through the seasons in german
MODULE Canada
VAR
  season : {spring, summer, fall, winter};
ASSIGN
  init(season) := spring;
  next(season) := 
    case
      season=spring : summer;
      season=summer : fall;
      season=fall : winter;
      season=winter : spring;
    esac;

MODULE Germany
VAR
  jahreszeit : {fruehling, sommer, herbst, winter};
ASSIGN
  init(jahreszeit) := fruehling;
  next(jahreszeit) :=
    case
      jahreszeit=fruehling : sommer;
      jahreszeit=sommer : herbst;
      jahreszeit=herbst : winter;
      jahreszeit=winter : fruehling;
    esac;

MODULE main
VAR 
  c : Canada;
  g : Germany;

-- It's spring in Canada iff it's Fruehling in Germany
-- true
SPEC 
  AG ((c.season=spring) <-> g.jahreszeit=fruehling)

------------------------------------------------------------
-- Version 3
-- contains two processes moving asynchronously
-- the first one cycles through the seasons in english
-- the second cycles through the seasons in german
MODULE Canada
VAR
  season : {spring, summer, fall, winter};
ASSIGN
  init(season) := spring;
  next(season) := 
    case
      season=spring : summer;
      season=summer : fall;
      season=fall : winter;
      season=winter : spring;
    esac;

MODULE Germany
VAR
  jahreszeit : {fruehling, sommer, herbst, winter};
ASSIGN
  init(jahreszeit) := fruehling;
  next(jahreszeit) :=
    case
      jahreszeit=fruehling : sommer;
      jahreszeit=sommer : herbst;
      jahreszeit=herbst : winter;
      jahreszeit=winter : fruehling;
    esac;

MODULE main
VAR 
  c : process Canada;
  g : process Germany;

-- It's spring in Canada iff it's Fruehling in Germany
-- false, because processes don't move in lockstep 
SPEC 
  AG ((c.season=spring) <-> g.jahreszeit=fruehling)

-- If it's spring in Canada then it'll always be Fruehling in Germany eventually
-- false, because Germany process may get ignored forever
-- need fairness constraint
SPEC 
  AG ((c.season=spring) -> AF g.jahreszeit=fruehling)


------------------------------------------------------------
-- Version 4
-- contains two processes moving asynchronously
-- the first one cycles through the seasons in english
-- the second cycles through the seasons in german
-- same as version 3, but with fairness constraint

MODULE Canada
VAR
  season : {spring, summer, fall, winter};
ASSIGN
  init(season) := spring;
  next(season) := 
    case
      season=spring : summer;
      season=summer : fall;
      season=fall : winter;
      season=winter : spring;
    esac;
FAIRNESS
  running

MODULE Germany
VAR
  jahreszeit : {fruehling, sommer, herbst, winter};
ASSIGN
  init(jahreszeit) := fruehling;
  next(jahreszeit) :=
    case
      jahreszeit=fruehling : sommer;
      jahreszeit=sommer : herbst;
      jahreszeit=herbst : winter;
      jahreszeit=winter : fruehling;
    esac;
FAIRNESS
  running

MODULE main
VAR 
  c : process Canada;
  g : process Germany;

-- It's spring in Canada iff it's Fruehling in Germany
-- false, because processes don't move in lockstep 
SPEC 
  AG ((c.season=spring) <-> g.jahreszeit=fruehling)

-- If it's spring in Canada then it'll always be Fruehling in Germany eventually
-- true
SPEC 
  AG ((c.season=spring) -> AF g.jahreszeit=fruehling)