module test

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

one sig Adam extends Man {}
one sig Eve extends Woman {}

fact Parenthood {

  -- 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 SocialNorms {
    -- spouse is symmetric
    spouse = ~spouse
    -- a man's spouse is a woman and vice versa
    Man.spouse in Woman && Woman.spouse in Man
    -- can't marry a sibling unless person is a child of Adam and Eve
    all p: Person | 
       (p.parents = Adam + Eve) or 
         no p.spouse.parents & p.parents
     -- can't marry a parent
    no p: Person | some p.spouse & p.parents
    -- parents are married
    all p: Person | p.parents.spouse = p.parents
    -- parents should be transitive and anti-symmetric
    all p1: Person  |
      p1 not in p1.^parents
    }

pred Show {some Person}

run Show for 10