Alloy Community

User login

Simple Library Model

whassan's picture
Date: 
Aug 2 2008
author: 
Wael Hassan

abstract sig date {
}

one sig one_week extends date{}
one sig two_week extends date{}
one sig three_week extends date{}

abstract sig user {
AttachedTo : one policy
}

abstract sig policy {
Allows: one date

}

sig Policy_A extends policy {
capacity: some book
}

sig Policy_B extends policy {
capacity: some computer + book
}

sig Policy_C extends policy {
capacity: some computer
}

abstract sig resource {
}

abstract sig book extends resource{}
abstract sig computer extends resource{}

one sig Book_1 extends book{}
one sig Book_2 extends book{}

one sig laptop_1 extends computer{}

one sig desktop_1 extends computer{}

/*
sig patientid2 extends ressources {}
sig U2 extends user{}
sig p2 extends policy{}
*/
assert both_sameuser{
}

//check both_sameuser for exactly 1 U, 1 p1, 1 p2, 1 patientid, 1 Z

assert both {
//no p:p | p.access in p.dined
}
check both for 1
pred show (){
}
//run show for exactly 1 U, 1 p1, 1 p2, 1 patientid, 1 Z //for exactly 1 U, 1
patientid, 1 p, 1 U2, 1 patientid2, 1 p2

run show


Syndicate content  

The development of this site is supported by the National Science Foundation under Computing Research Infrastructure Grant No. 0707612.

Theme originally designed by Chris Herberte