Oefenzitting 5 oefening 2
Issue #908
invalid
Turn(StartPlayer, Start).
!t: GameOver(t) <- ! h: Nb(h, 0, t).
! t p : Turn(p, Next(t)) <- ~ Turn(p, t) & ~ GameOver(t).
! t p : Turn(p, Next(t)) <- Turn(p, t) & GameOver(t).
! t p : Winner(p, t) <- GameOver(t) & Turn(p, t).
//Werkt niet
//! p t: Winner(p, Next(t)) <- ~ Turn(p, t) & ! h : Nb(h, 0, t) & ~ GameOver(t).
//! t : GameOver(t) <- ? p : Winner(p, t).
//! t : GameOver(Next(t)) <- GameOver(t).
Comments (7)
-
-
Bron is een student die een modellering had die volgens mij OK was, maar waar geen model uitkwam. Heb er lang op zitten zoeken en niets gevonden. Heb als laatste resort de student een issue laten aanmaken.
In bovenstaande issue werkt de definitie, maar de alternatieve definities van Winner en GameOver werken niet (wanneer dit toch geen invloed zou moeten hebben op satisfiability)
Ik ga Ingmar/Matthias/Laurent er eens mee lastigvallen als ze terugzijn.
-
Misschien moet je de niet-werkende alternatieve definities ook op bitbucket plaatsen... Want nu is de issue nogal nutteloos aangezien hij niet reproduceerbaar is met deze info.
-
De niet-werkende versie is gecommentarieerd in de bijgevoegde file
-
En als ik die uncomment is hij nog steeds satisfiable...
-
- changed status to invalid
Dit is geen bug, gewoon een slechte modellering:
Op tijdstip x neemt een persoon de laatste match
Op tijdstip x+1 zijn alle stacks dus leeg
Op tijdstip x+2 hebben we dus een winner
Op tijdstip x+2 is het dus pas gameover
Dit betekent dat er op tijdstip x+1 geen actie kan gebeuren, maar wel een actie moet gebeuren (het is nog niet gameover).
In het algemeen, als je in een LTC theorie ergens ketens van Next'en kan maken die meer dan twee levels diep zijn (in dit geval:
Turn(t) -> gameover(t-1) -> Winner(t-1) -> Turn(t-2)
Dan is dat iets verdacht ;-)
De juiste regel voor winner zou hier zijn:
! p t: Winner(p, t) <- Turn(p, t) & ! h : Nb(h, 0, t). -
Merci, ik had dat niet gezien.
- Log in to comment
Een beetje bijkomende info? Wat werkt er niet? Dit runt op de online IDE prima...