project-planning.tla

------------------------------ MODULE Project ------------------------------
EXTENDS Naturals, Sequences
VARIABLES devs, projects, time
vars == << devs, projects, time >>




ProductName =={"PA", "PB", "PC","PD"}
DevName == {"J","B"}
DStatus == {"Busy","Free"}
PStatus == {"Done", "TODO", "Work"}




dep(a,b) == << a, b >>

Deps =={ dep("PA", "PB"),
         dep("PB", "PC"),
         dep("PB", "PD") }


DependsOn(a,b) == 
 /\<< a , b >> \in Deps



Product == [ time: Nat, 
             status : PStatus ]


SetProjects == LET f == [p \in ProductName |->[ time |-> 0 , status |-> "TODO"]] 
               IN [[[[f EXCEPT !["PA"] = [ @ EXCEPT !.time = 1] ] 
                        EXCEPT !["PB"] = [ @ EXCEPT !.time = 1]] 
                        EXCEPT !["PC"] = [ @ EXCEPT !.time = 2]]
                        EXCEPT !["PD"] = [ @ EXCEPT !.time = 2]]
              

Init ==
 /\devs = [name \in DevName |-> "Free" ]
 /\ projects = SetProjects
 /\ time = 0
 
DepsComplete(proj) == 
     ( \A p \in ProductName : ( DependsOn(proj, p) => projects[p].status = "Done") )

DepsIncomplete(proj) == 
     ( \A p \in ProductName : ( DependsOn(proj, p) => projects[p].status # "Done") )



WorkOnProject(dev,proj) ==
  /\ devs[dev] = "Free"
  /\ projects[proj].time # 0
  /\ projects[proj].status = "TODO"
  /\ DepsComplete(proj) 
  /\ devs' = [ devs EXCEPT ![dev] = "Busy"]
  /\ projects' = [ projects EXCEPT ![proj].status = "Work" ]

CompleteProject(dev,proj) ==
  /\ devs[dev] = "Busy"
  /\ projects[proj].status = "Work"
  /\ projects[proj].time = 0
  /\ devs' = [ devs EXCEPT ![dev] = "Free"]
  /\ projects' = [ projects EXCEPT ![proj].status = "Done"]


Work == ( \E p \in ProductName :
                    \E d \in DevName : WorkOnProject(d,p))
                    
Complete == ( \E p \in ProductName :
                    \E d \in DevName :CompleteProject(d,p))                                     


ProjectCantStart(proj) == 
  /\ projects[proj].status = "TODO"
  /\ DepsIncomplete(proj)

AllWorkIsWaiting ==
(*  /\ \E p \in ProductName : ProjectCantStart(p) *)
  /\ \E d \in DevName :  devs[d] = "Free"
  /\ \E d \in DevName :  devs[d] = "Busy"  
  /\ \E p \in ProductName :
      projects[p].status = "Work" /\
      projects[p].time # 0 /\ 
      projects' = [projects EXCEPT ![p].time = @ -1]
        
  




EveryoneIsBusy == 
  /\ \A d \in DevName : devs[d] = "Busy"
  /\ \E p \in ProductName : ( projects[p].status # "Done"
                               /\ projects[p].status # "TODO"
                               /\ projects' = [ projects EXCEPT ![p].time = @ -1 ]
                               /\ projects[p].time > 0)
  
                             

IncrementTime == (time' = time + 1)

Finished == ( \A p \in ProductName : projects[p].status = "Done" /\ UNCHANGED vars)



Next == 
  (Work /\ IncrementTime) \/
  (Complete /\ IncrementTime) \/               
  (EveryoneIsBusy /\ IncrementTime /\ UNCHANGED << devs >> ) \/
  (AllWorkIsWaiting /\IncrementTime /\ UNCHANGED << devs >> ) \/ 
  (Finished  )


TypeOK == 
  /\ devs \in [DevName -> DStatus]
  /\ projects \in [ProductName -> Product]
  /\ time \in Nat

Termination == <> ( \A p \in ProductName : projects[p].status = "Done")

=============================================================================
\* Modification History
\* Last modified Fri Apr 02 20:37:52 CDT 2021 by scott

\* Created Fri Apr 02 16:32:07 CDT 2021 by scott