module test

abstract sig Person {spouse: lone Person, parents: set Person}
sig Man, Woman extends Person {}
one sig Eve extends Woman {}
one sig Adam extends Man {}

pred Parenthood {
    -- no person is their own ancestor
    no p: Person | p in p.^parents

    -- every person except Adam and Eve has a mother and father
    all p: Person - (Adam+Eve)| one mother: Woman | one father: Man |
        p.parents = mother + father
    }

fact enforceParentHood {Parenthood}

pred checkSocialNorms[sp: Person -> lone Person] {
    -- spouse is symmetric
    sp = ~sp
    -- a man's spouse is a woman and vice versa
    Man.sp in Woman && Woman.sp in Man
    -- can't marry a sibling unless person is child of Adam and Eve
    all p: Person |
       (p.parents = Adam + Eve) or
         no p.sp.parents & p.parents
    -- can't marry a parent
    no p: Person | some p.sp & p.parents
    -- parents are married
    all p: Person | p.parents.sp = p.parents
    }

fact enforceSocialNorms {checkSocialNorms[spouse]}

pred Show {}


pred getMarried  [p1, p2: Person, spUpdated: Person -> lone Person]  {
    (no p1.spouse and no p2.spouse 
     and ((p1 in Woman and p2 in Man) or (p1 in Man and p2 in Woman))
     and no p1.parents & p2.parents)

     implies spUpdated = spouse + p1->p2

     else spUpdated = spouse
  }

pred getMarriedNotCorrect[spUpdated: Person -> lone Person] {
   some p1, p2: Person |
    getMarried[p1, p2, spUpdated] and not checkSocialNorms[spUpdated]
  }

run getMarriedNotCorrect for 10