Violate fact in alloy

Question

I'm creating bell lapadula and this is my code.

abstract sig classificaion{}
one sig classified extends classification{}
one sig unclassified extends classification{}
sig user{ level: one classification,
    r,w: set object}
sig object{ sec: one classification}
fact policy1{no((classified.~sec).~r & unclassidied.~level)}
fact policy2{no((unclassified.~sec).~w & classifed.~level)}

I want to test policy1. So i added this in my code to check if it will violate policy1. But i keep getting error in "level:"

one sig usera extends user{}{
level: one classified,
r: set objecta
}
one sig objecta extends object{}{
sec: one unclassified
} 

Answer 1

You probably want to write :

one sig usera extends user{}{
level= classified
r=objecta
}
one sig objecta extends object{}{
sec= unclassified
} 

Note that a signature fact contains formulas (expressions that evaluates by true or false), that need to hold for any instance of the object.

In that sense, writing level = classified means that the level of every usera atom (bound to be only one) is classified.