Alloy

Example 1

This is from the website, a simple model of a file system:

module chapter4/filesystem ----- The model from page 125

abstract sig Object {}

sig Dir extends Object {contents: set Object}

one sig Root extends Dir { }

sig File extends Object {}

fact {
   Object in Root.*contents
   }

assert SomeDir {
   all o: Object - Root | some contents.o
   }
check SomeDir // This assertion is valid

assert RootTop {
   no o: Object | Root in o.contents
   }
check RootTop // This assertion should produce a counterexample

assert FileInDir {
   all f: File | some contents.f
   }
check FileInDir // This assertion is valid

Screen Shots

Edit window, to edit models, and the analysis output:

Viewing a counter example: