https://github.com/ISCAS-PMC/ePMC/blob/4b1bdca2c58f209ee5a8401fdaff23515510a079/plugins/propertysolver-pctl/src/main/java/epmc/propertysolver/PropertySolverExplicitPCTLUntil.java#L178 should the second parameter be 'op2'?