Trio2Promela: a model checker for temporal metric specifications