Added initial CTL patterns library and added WeakUntil operator to CTL library, set up new model that uses new pattern library