open util/ordering[Aika] as A
sig Aika{}

abstract sig Olio{}
abstract sig Toimija extends Olio{perusOikeudet:set Viesti}

sig Käyttäjä extends Toimija{}
 {perusOikeudet={v:(Lue+Kirjoita)|v.lähettäjä=this and v.kohde.omistaja=this}
                             +{v:Käännä| v.lähettäjä=this}}
one sig Kääntäjä extends Toimija{}
 {no perusOikeudet}

abstract sig Viesti
   {lähettäjä:Toimija, kohde:Olio, aika:Aika,siirtoOikeudet:set Viesti}
   {this in Oikat[lähettäjä]
    siirtoOikeudet in Oikat[lähettäjä]}

fun Oikat[t:Toimija] : set Viesti {
  {v:Viesti|v in t.perusOikeudet
                 or (some v2:Viesti| v2.kohde=t and v in v2.siirtoOikeudet)}
}

sig Lue,Kirjoita extends Viesti
  {}
  {kohde in Tiedosto}

sig LisääLoppuun extends Kirjoita{}

sig Käännä extends Viesti
 {sorsa:Tiedosto, binääri:Tiedosto}
 {kohde=Kääntäjä and lähettäjä in Käyttäjä}

sig Tiedosto extends Olio{}

sig KäyttäjänTiedosto extends Tiedosto{omistaja:Käyttäjä}
//one sig Loki          extends Tiedosto{}

/*
fact Aluksi{
 let t0=A/first[] |
 no v:Viesti | v.aika=t0
}*/

fact Askel{
 all t:Aika |
 let t1=A/next[t] |
  {
    (no k:Käännä | k.aika = t) =>
         (all v:Viesti | v.aika=t1 => v.lähettäjä in (Käyttäjä))
    else (all k:Käännä | AjaKääntäjä[k])
  }
}

pred AjaKääntäjä[k:Käännä]{
 let t1 = A/next[k.aika] |
 {
 // some v:LisääLoppuun | v.aika=t1 and v.lähettäjä = Kääntäjä and v.kohde=Loki
  some v:Kirjoita - LisääLoppuun  | v.aika=t1  and v.kohde=k.binääri and
														v in Oikat[Kääntäjä]
  some v:Lue                                 | v.aika=t1 and v.kohde=k.sorsa and
											 			v in Oikat[Kääntäjä]
 }
}

//assert LogiinVainLisätään{
//   all v:Viesti | v.kohde = Loki => (v in LisääLoppuun) }

assert  VainKäyttäjäMuuttaa{
 some Käyttäjä =>
  all t:KäyttäjänTiedosto | (some v:Viesti|v.kohde=t) =>
	(some v2:Viesti|v2.lähettäjä=t.omistaja and t in v2.(kohde+sorsa+binääri))
}

pred Show {one Käännä and #Käyttäjä>1 and #KäyttäjänTiedosto>1}
check VainKäyttäjäMuuttaa for 9
run Show for 8
run AjaKääntäjä for 7 but exactly 2 KäyttäjänTiedosto
//check LogiinVainLisätään for 5