One can add ltl formulas on the command line. The ltl formula is copied directly into the create promela file. All spin inline ltl formulas are supported. A signal value inside a CD is referenced as CD<num>_<sig-name>