Experiences with colored predicate-transition nets for specifying and prototyping embedded systems