PS1 sample solutions (assembled from student submissions)
screen shots of sample instances have been omitted
total points: 30

------------------------------------------
1.1 (Punya Biswal) - 3 points

a. pred safe() {all c: Cell | lone c. follow Doris Daybody (including y babyryone except odule dorisday
sig Person { loves: one Person }
one sig Baby in Person {}
one sig Me in Person {}
fact {
     all p : Person - Baby | p.loves = Baby
     -- originally all p: Person | p.loves = Baby
     no p: Person - Me | p in Baby.loves
}
assert IamBaby {Me = Baby}
check IamBaby

------------------------------------------
2.2 (Janis Sermulins) - 4 points

a) the model is indeed inconsistent!


b)

sig Person { shaves: set Man }
sig Man extends Person {}
sig Woman extends Person {}
one sig Barber extends Man {}
fact {
     Barber.shaves = {m: Man | m not in m.shaves && (no w: Woman | m
     in w.shaves) }
     }


I modify the model so that barber shaves everyone who does not shave himself or who is not shaved by some woman.

c)
sig Man { shaves: set Man }
sig Barber extends Man {}
fact {
     Barber.shaves = {m: Man | m not in m.shaves}
     all m: Man | some p:Man | m in p.shaves
     all m: Man | #(shaves.m) < 2
     no Barber
     }


I modify the model, so that there is no barber and also everyone is shaved by someone
and nobody is shaved by more than one person.

d)
sig Man { shaves: set Man }
sig Barber extends Man {}
fact {
     Barber.shaves = {m: Man | m not in m.shaves}
     all m: Man | some p:Man | m in p.shaves
     all m: Man | #(shaves.m) < 2
     }


Now I allow multiple barbers and also enforce that everyone is shaved by someone,
And that nobody is shaved by more than one person. Here is a simple solution: two
barbers shave each other, and one barber shaves a non-barber.

------------------------------------------
2.3 (Craig) - 2 points (+1 bonus for writing own model or significantly modifying sample solution)

* a. We start with the signature for a person,

     sig Person
     {
        shook: set Person,
        partner: one Person
     }

     the fields of which are obvious. Then we add the essential facts
     for the model:


     fact
     {
        /* nobody shakes his/her own hand */
        all p: Person | p not in p.shook

        /* the partner relation is symmetric, and nobody is his/her own partner;
         * together these guarantee the necessary pairing relationship */
        partner = ~partner
        no partner & partner.partner

        /* nobody shakes his/her partner's hand */
        all p: Person | p.partner not in p.shook

        /* the handshaking relation is symmetric */
        shook in ~shook
     }

     These are all the facts that need to hold for any number of
     people. For the specific number of people, 10 in this case, we
     add another fact:

     fact nhs
     {   
        #Person = 10

        some p: Person | #p.shook = 0
        some p: Person | #p.shook = 1
        some p: Person | #p.shook = 2
        some p: Person | #p.shook = 3
        some p: Person | #p.shook = 4
        some p: Person | #p.shook = 5
        some p: Person | #p.shook = 6
        some p: Person | #p.shook = 7
        some p: Person | #p.shook = 8   
     }

     This is somewhat awkward, but it is correct and its behavior is
     obvious (side note: dealing with Int vs. int was much more confusing
     and made it difficult to achieve the same goal). Given these, we
     run an empty show() predicate for 10 Person's, and we get the
     instance, given as text in handshake_a.instance.txt (this is much
     easier to read than the visualization). The "me" person in the
     problem should be the only one not in the skolem constants; this
     is Person_9. Person_9's partner is Person_4, who shook 4 hands,
     so that is our answer. This also matches the pattern for lesser
     numbers of Person's: when 8, the answer is 3; when 6, 2; when 4,
     1.

* b. We add another signature: "one sig Me extends Person {}",
     representing the "me" in the problem. We modify the "nhs" fact
     above slightly, to replace every occurance of "Person" with
     "Person-Me". Finally, we check the assertion:

     assert wife_shakes_four { #Me.partner.shook = 4 }

     This updated model describes the problem more precisely. Since
     the assertion always holds, we find that 4 is the unique
     solution.

module handshake_b
sig Person
{
   shook: set Person,
   partner: one Person
}
one sig Me extends Person {}
/*
 * require essential facts for the model.
 */
fact
{
   /* nobody shakes his/her own hand */
   all p: Person | p not in p.shook

   /* the partner relation is symmetric, and nobody is his/her own partner;
    * together these guarantee the necessary pairing relationship */
   partner = ~partner
   no partner & partner.partner

   /* nobody shakes his/her partner's hand */
   all p: Person | p.partner not in p.shook

   /* the handshaking relation is symmetric */
   shook in ~shook
}
fact nhs
{   
   #Person = 10

   some p: Person-Me | #p.shook = 0
   some p: Person-Me | #p.shook = 1
   some p: Person-Me | #p.shook = 2
   some p: Person-Me | #p.shook = 3
   some p: Person-Me | #p.shook = 4
   some p: Person-Me | #p.shook = 5
   some p: Person-Me | #p.shook = 6
   some p: Person-Me | #p.shook = 7
   some p: Person-Me | #p.shook = 8   
}
assert wife_shakes_four { #Me.partner.shook = 4 }
check wife_shakes_four for 10

------------------------------------------
3.1 (Martin Ouimet) - 7 points

A few clarifications about this question: by the formal definition of automaton, there is
only 1 initial state. Having more than 1 initial state implies non-determinism. For the sake
of this question though, we assume that a finite state automaton can have more than 1
initial state as mentioned in the problem statement.

module automaton

sig state {successors: set state}
some sig initial extends state {}

pred deterministic() {
     all s: state | lone s.successors
}

pred nondeterministic() {
     some s: state | #s.successors > 1
}

pred unreachable() {
     some s: state - initial | all t: initial | s not in t.(^successors)
}

pred reachable() {
     all s: state - initial | all t: initial | s in t.(^successors)
}

pred connected() {
     all disj s, t: state | s in t.(^successors)
}

pred deadlock() {
     some s: state - initial | all t: initial | s in t.(^successors) and no s.successors
}

pred livelock() {
     some s: state - initial | all t: initial | s in t.(^successors) and some ^(successors - univ -> s) & iden and some (^(successors - univ -> s) & iden).univ & t.(^(successors - univ -> s))
}

pred test() {
       --deterministic()
       --nondeterministic()
       --unreachable()
       --reachable()
       --connected()
       --deadlock()
       --livelock()
}

run test for 5

------------------------------------------
4.1 (Lucy Mendel) - 12 points

see separate file