We modify the reader to have an infinite loop but model checking completes successfully. When I enable the generated Termination property I see that the system does not terminate (as expected), but I was confused before digging deeper and discovering this. At first, I expected some sort of error when running model checking due to the system generating an infinite number of "actions". After thinking about this more and knowing the behavior, I think this is because there can be a finite number of states to check even if the path through those states does not terminate - but I'm not 100% sure.
Maybe it's worth clarifying for the inexperienced reader that the model checking can complete even if the modeled system does not terminate and helping to build the mental model of why that is the case?
referring to here
We modify the reader to have an infinite loop but model checking completes successfully. When I enable the generated
Terminationproperty I see that the system does not terminate (as expected), but I was confused before digging deeper and discovering this. At first, I expected some sort of error when running model checking due to the system generating an infinite number of "actions". After thinking about this more and knowing the behavior, I think this is because there can be a finite number of states to check even if the path through those states does not terminate - but I'm not 100% sure.Maybe it's worth clarifying for the inexperienced reader that the model checking can complete even if the modeled system does not terminate and helping to build the mental model of why that is the case?