How to check whether a specific instance is compliant with a model

Posted on: Sun, 02/14/2010 - 07:29

Joined: 2009-10-04

Points: 34

How to check whether a specific instance is compliant with a model

I am looking for a generic modeling idiom to check specific instances within Alloy. That is, to specify an Alloy model that consists of a "model" part and a "specific instance" part, and ask Alloy whether the instance part is consistent with the model part.

For example, in a model of a hierarchical file system with some constraints on the depth and size of folders, I would like to specify (in addition to the "model part" within the Alloy model), a specific instance, say, three folders, each with 5 files and 2 empty directories. Maybe the "model" says directories should not be empty and in my "instance" I have empty directories, or maybe the "model" says there is no more than one empty directory in the entire system and in my "instance" I have two, etc. A more difficult example would be that in the "model", a "directory" is a subclass of "file" while in the "instance", the directories are not files (although otherwise they have the same attributes).

I want to "assert" that this "instance" is compliant with the "model" (that is, that if I run the model, I may get this instance from the analyzer) and have Alloy check this assertion.

It seems that this problem is within the expressive power of Alloy. So, is there an example of such a setup or better a generic idiom for that, or should I try to develop one myself?

Thanks for your thoughts.

S

Posted on: Mon, 02/15/2010 - 18:31 #1

cmsmcq

Joined: 2008-07-25

Points: 77

Checking specific instances in this way does not seem high on the priority list of the Alloy design (so I don't remember finding examples of how to do it in Daniel Jackson's book or in the online documentation). But it's possible.

One way I've done this in the past is to put the instance in a separate .als file (to keep it out of the 'real' model), import the 'real' model, define singleton classes for all the entities that should exist in the instance, and constrain them to have the appropriate interrelations. Another way is to define a predicate in which the various entities required are asserted to exist with the appropriate constraints. The conformance of the instance with the model is then tested by using a run predname command; if an instance of the predicate is found, it's consistent with the model, and otherwise it's not. You can underspecify the example, too, so that there may be multiple instances of the predicate.

An example of the second style can be found in section 1.4 of a working paper I produced in 2006 with Alloy models of the then-current drafts of the specification for the XML processing language XProc (XML form, HTML form).

There may be better and more convenient idioms, but this one has worked for me.

--C. M. Sperberg-McQueen
cmsmcq@blackmesatech.com
http://cmsmcq.com/mib

Search

Navigation

User login

How to check whether a specific instance is compliant with a model