A Compositional Trace-Based Semantics for Probabilistic Automata