Learning Alloy: How to Define Objects Generated by Events

If you are software developer, you often implement the object which generated by some other event. But when I represent such objects on Alloy, I always make a mistake. Why? Now I've got the reason. Here it is.

Modeling a "login page".

Generally, authentication in web application uses some session system. In this case, I assume that a session object is generated by "authentication succeeded" event.

Here are the members and their relations.

enum Password {correct, incorrect}
some sig UserAccount {
  password: one correct
}
sig Session {
  whose: disj one UserAccount
}
sig Visitor {
  signIn: disj lone Session,
}
sig InputForm {
  currentVisitor: disj one Visitor,
  targetUser: one UserAccount,
  input: targetUser -> one Password
}

fact {
  all sess:Session | sess in Visitor.signIn
}
fact {
  all vis:Visitor |
   vis.signIn.whose in currentVisitor.vis.targetUser
}

From here, step into the next: defining behavior of LoginForm.

My mistake: "Okay, I will represent a behavior of the LoginForm as 'pred'."

The idea which I came up with first is that I treat a input from users as arguments of function like I used to do in procedural programming. I had sensuously understood that pred is like a function on procedural programming.

pred login[f:InputForm] {
  f.targetUser.(f.input) = f.targetUser.password 
    implies f.currentVisitor.signIn in Session
    else f.currentVisitor.signIn = none
}
check Login {
  all f:InputForm |
    !login[f]
    implies 
      f.targetUser.(f.input) = incorrect 
      && f.currentVisitor.signIn = none
}

But this modeling is incorrect. Alloy showed some counter examples. This model allows it to generate a session object despite of the password is incorrect.

result on Evaluator:

I rewrote the pred many times and finally threw away the first perspective.

A different angle

I saw a session object is generated by success of a authentication. So I tried to represent the cause-and-effect relationship between the session object and the authentication in a direct way. It was not a good idea. Because there are no idioms to represent cause-and-effect relationships in Alloy.

Okay, I'll forget the cause-and-effect relationship. Instead of representing it, I wrote variations of the state consisting of valid elements.

fact {
  all f:InputForm |
    f.targetUser.(f.input) = f.targetUser.password 
      iff f.currentVisitor.signIn in Session
    ||
    f.targetUser.(f.input) != f.targetUser.password 
      iff f.currentVisitor.signIn = none
}

Oh, I got it despite of the body of constraints was almost same.

I found it must be written as fact what causes what by throwing away the sense of procedural programming and thinking about state.

The Takeaway

All of event processing contains cause-and-effect relationships. But when you will represent it in Alloy, there is no need to define any cause and effect. All you need is thinking about state. And cause-and-effect relationship can be represented by state.

Future work

I represented the rules of authentication and session in web application from a macroscopic viewpoint. So, what makes the rules work? It is every implemented module of the web application. If I represent the specifications of those modules, I must define not only the rules but also events or state transition by using more complicated techniques.

(Special thanks to Lola A.)