In this case, "some" modifies "X", meaning that X should be non-empty. However, "lone" still modifies "p", implying that the cardinality of p <= 1. In other words, this constraint says that there's at most one "p" in the non-empty set "X" such that "F" holds true.
Higher Order quantification in Alloy
-
01-12-2021 - |
Question
I was reading about higher order quantification in alloy, and saw the following: lone p: some X| F
now, I am confused if the keyword 'some' modifies p or X. Does it mean X should be nonempty or does it mean that the cardinality of p should be >=1.
Solution
Licensed under: CC-BY-SA with attribution
Not affiliated with StackOverflow