This package contains hand coded examples for temporal logics specifications.