my_digital_garden/4a1s/MFES/PL - Aula 8.md

https://why3.lri.fr/try/?name=test.mlw&lang=whyml&code=AN7HpJ4Recall1the4officeyassignment%2F4puzzle2from3Fichaz17r3whereBHz44people1areydistributed%2F0byz35officesl2such2that7vH7s2each4person0is6assignedza4singleVHm2Nuno1and3Pedro0do1not3share0anlHl0If1Ana1hasoo2just1for5herselfV2then0so2doesdHg5Officesyaccomodate%2F0at2most1twouIHHuBuMg0if5running2Why32withXyappropriate%2F1SMT4solverlBH0inuByfollowing%2F1you2will0be2able0to5inspect5counterASA6examplesBH2when6adequate7tBNHHz1s3Modele5problemuI6definingVVypredicate%2FBKuQ5writingza1set0of4axiomsfH0In3orderV5expressc3thirdyrequirement%2F3above7r4defineBHfc7h3alonesyexpressing%2Ful5someoneuMg2onlyBH6occupierXSuVWHEz2s2ShowikTuGuPyinconsistent%2Fu0u3hBKu12goalhHEz3s2Find1outuhfunyproperties%2F4followuDpb7vL7suP3MariaPuKR1One7ruT1sheukukLfu7u7u7u8iTDccuOusuLuMu9lbbXmuSaBL5equally2haveusiiidBMDHz4s5Finallyfyformulate%2Fg3provezau85statingVBLuUuU1onef1mayvG3emptyd1For2thisc3first3writeduvBHuwdVfvAg7nzieAzesuzu%2FvO4anyone7ItBHDz5n5Producefyalternative%2Fyformalization%2F3usingV5insteadvEVVpBLr3logic6functionU3givesvB4uniqueRXXBHuIuIY4Repeat1allk6previous3stepsuXvWVlDN7JoBNNNN4moduleuQNF2typec7yu7781Twos3ThreeHnanu%2Fou%2FsvBsvANHveyhasOffice%2F7nk7orerNH3axiom0A1B7v4forallzprAlV4existszopAjphmoHj0A2BmjorAj7r0o10o2BphhJhln7O3qqm7MzoUqFHfzBBiBfnoqhhiVngqUlgLo7RzqDHVurUbfAZUZbWAoAaap0p1plpJjbikiapkpbngpNFXzCgdPlrWHnzDBnBbk0p20p3ApZRdqXXJakoZqjqqqjqdLnam7XuqqnqsrpNMBvHysanity%2Btest%2Fg3falseuAA3checkuzvk3model3makes3senseAvpHHi0g1BiBZvvvrYv3qHm0g2mPvyrQQ7nhv1nOqvxq7oeBLvvvxAhAhhkvyoiqcqBNDvxvQdzoiif7yazpAoAvxdvQjenijHH3lemmayatMostOneEmpty%2FBjBiXcqBegdoarnXLpbqNN1endBNNNNvnyOffices%2BFn%2FBNDvqinv978vosvoHnTnv%2Bov%2BsOsONHvZhPkSVBpNHvqzBqqjvprhHHv8v4izplAhhcOzooAi7tpvpplpJqfjOlrqrpHFbzCkeWkraNHnzDnBfkvrvqpddoAeAnv8qAqAmqpAqAqgLdnprovprpBpBrnNNDv0vpBhBvpBNHqvxBqnOUv9fXpHlvxBllVkrOkrlprUNHOv27nOiAn7olRzpAoAQQmpUkHHv0v0Blkv0v0qkjeov8rnZLpeqNNv0NNNN
```c
(*
    Recall the office assignment puzzle from Ficha 1, where 
    4 people are distributed by 3 offices, such that:
    - each person is assigned a single office
    - Nuno and Pedro do not share an office
    - If Ana has an office just for herself, then so does Pedro
    - Offices accomodate at most two people
    
    Recall that, if running Why3 with an appropriate SMT solver, 
    in the following you will be able to inspect counter-examples 
    when adequate. 

    
    1. Model the problem by defining an appropriate predicate 
       and writing a set of axioms.
       In order to express the third requirement above, define 
       a predicate "alone" expressing that someone is the only 
       occupier of an office.
       
    2. Show that the axioms are not inconsistent by writing an 
       appropriate goal.
       
    3. Find out if the following properties follow from the axioms:
        - If Maria is assigned office One, then she will be
            the only occupier of that office.
        - If Ana and Nuno share an office, then Maria and Pedro will 
            equally have to share an office. 
    
    4. Finally, formulate and prove a goal stating that 
        at most one office may be empty. For this, first write a predicate 
        expressing that an office is empty (i.e. not assigned to anyone). 
        
    5. Produce an alternative formalization using, instead of a predicate, 
        a logic function that gives the unique office assigned to 
        each person. Repeat all the previous steps with this formalization.
    
*) 



module Offices

  type office = One | Two | Three
  type person = Ana | Nuno | Pedro | Maria

  predicate hasOffice (person) (office)

  axiom A1 : forall p:person. exists o:office. hasOffice p o
  axiom A2 : forall p:person, o1 o2 : office.
    hasOffice p o1 /\ hasOffice p o2 -> o1 = o2
  
  axiom B : forall o1 o2 : office. hasOffice Pedro o1 /\ hasOffice Nuno o2 ->
      o1 <> o2
  
  predicate alone (p:person) = forall o:office. forall p1:person.
    (hasOffice p o) /\ hasOffice p1 o -> p = p1

  axiom C : alone Ana -> alone Pedro
  axiom D : forall p1 p2 p3: person, o:office.
    hasOffice p1 o /\ hasOffice p2 o /\ hasOffice p3 o ->
        p1 = p2 \/ p1 = p3 \/ p3 = p2

  goal sanity_test : false (*check if the model makes sense*)
  
  goal g1 : hasOffice Maria One -> alone Maria
  goal g2 : forall o1:office. (hasOffice Ana o1 /\ hasOffice Nuno o1) -> 
      exists o2:office. hasOffice Pedro o2 /\ hasOffice Maria o2 

  predicate empty (o:office) = forall p:person. not (hasOffice p o)
  
  lemma atMostOneEmpty : forall o1 o2: office. empty o1 /\ empty o2 ->
      o1 = o2

end 







module Offices_Fn 

  type office = One | Two | Three
  type person = Ana | Nuno | Pedro | Maria

  function office (person) : office

  axiom B: office Pedro <> office Nuno
  
  predicate alone (p:person) = forall o:office. forall p1:person.
    p1 <> p -> office p <> office p1
    
  axiom C: alone Ana -> alone Pedro

  axiom D: forall p1 p2 p3: person. p1<>p2 /\ p1<>p3 /\ p2<>p3 ->
      office p1 <> office p2 \/ office p1 <> office p3


  goal sanity_test : false 

  goal g1 : office Maria = One -> alone Maria
  goal g2 : office Ana = office Nuno -> office Maria = office Pedro

  predicate empty (o:office) = forall p:person. office p <> o
  
  lemma atMostOneEmpty : forall o1 o2: office. empty o1 /\ empty o2 ->
      o1 = o2

end
```