diff --git a/reports/discussion.tex b/reports/discussion.tex index 0f2b23f..5b9f0e9 100644 --- a/reports/discussion.tex +++ b/reports/discussion.tex @@ -62,7 +62,7 @@ \paragraph{Value of producing examples.} Even though checking accountable safety proved to be challenging, our specifications are not limited to proving the property. They are also quite useful for producing examples. For -instance, both Apalache and Alloy were able to quickly produce examples of +instance, both Apalache and Alloy are able to quickly produce examples of configurations that contain justified and finalized checkpoints. We highlight this unique value of specifications that are supported by model checkers: