Open buggsley opened 8 years ago
When CTL property fails, should generate an error trace. The idea is based on finding a witness. For EG, this means return one strongly connected compoent. For EU, only one path back to the initial state.
When CTL property fails, should generate an error trace. The idea is based on finding a witness. For EG, this means return one strongly connected compoent. For EU, only one path back to the initial state.