Suppose we have two users, Peter and Betsy, and a single printer device Printer. Both users perform several tasks, and every now and then they want to print their results on the Printer.
Since there is only a single printer, only one user can print a job at a time. Suppose we have the following
atomic propositions for Peter at our disposal:

Peter.request -- indicates that Peter requests usage of the printer;
Peter.use -- indicates that Peter uses the printer
Peter.release -- indicates that Peter releases the printer

For Betsy similar predicates are defined. Specify in LTL  and/or using assertions the following properties:

Mutual exclusion, i.e. only one user at a time can use the printer
Finite time of usage, i.e. a user can print only for a finite amount of time
Absence of individual starvation, i.e. if a user wants to print something, he/she eventually is able to do so
Alternating access, i.e. users must strictly alternate in printing

Make a Promela model that satisfies (some of the) properties above.