CODEWITHSUNDEEP
alloy
Roger Costello
Roger Costello

Reputation: 3209

How to express validity?

I am creating an Alloy model of the iCalendar data format.

An iCalendar file contains properties. There are a lot of codependencies among the properties. I want to see if anything breaks when a property is removed (i.e., when the property is constrained to zero occurrences).

I want to write an assert and have the Alloy Analyzer search for counterexamples, but I am struggling with how to write the assert. I want the assert to say something like this:

If property X is removed (i.e., property X is constrained to zero occurrences), there are no instances that are invalid as a result of removing X.

In pseudocode, I want this:

assert NoProblemFilteringX {
    (no prop: X | prop in iCalendar.properties) => all instances are still valid
}

Would you provide some guidance on formulating the desired assert, please?

Upvotes: 1

Views: 61

Answers (1)

Loïc Gammaitoni
Loïc Gammaitoni

Reputation: 4171

Suggestion:

  1. Write your codependency checks in a predicate taking as parameter a set of properties. The predicate holds iff the codependencies are satisfied amongst those properties given in parameter.

  2. Rewrite your fact ensuring those codependencies so as to call this predicate with the set of all iCalendar properties as parameters.

  3. Call this predicate in the assert while this time giving iCalendar.properties - X as parameter

Upvotes: 2

Related Questions