Alloy dynamic modelling with predicates

Question

I am trying to model in alloy a system where the users can make comments on forum threads. I want to describe with a predicate a situation where a new comment is added to a forum thread.

This is what I have done:

//other signatures (including User, DateTime, ...)

sig ForumThread {
    title: one String,
    datePosted: one DateTime,
    author: one User,
    content: one String,
    comments: set Comment
}

sig Comment {
    content: one String,
    datePosted: one DateTime,
    author: one User,
}

//other signatures ...

fact allCommentsAreInAThread{
    all c: Comment | one t: ForumThread | c in t.comments
}

//other facts ...

pred addComment[t, t': ForumThread , c: Comment ] {
    t'.comments = t.comments + c
    t'.datePosted = t.datePosted
    t'.author = t.author
    t'.content = t.content
    t'.title = t.title
}
run addComment

//...

Now, this predicates is consistent (as the analyzer said). However, i think that it can be true only in trivial models, that are the ones where c is already in t.comments and where t is exactly t’. This, because the first fact says that a Comment must always have to be exactly in a ForumThread. Is what i am saying true? If yes, is there a way i can model what i am trying to do without eliminating the fact (since it wouldn't have sense to have comments that are in nothing)?

Answer 1

However, i think that it can be true only in trivial models, that are the ones where c is already in t.comments and where t is exactly t’.

Indeed, because of allCommentsAreInAThread, which is a fact (= an axiom) so any model necessarily respects it.

is there a way i can model what i am trying to do without eliminating the fact (since it wouldn't have sense to have comments that are in nothing)?

You must remove the fact as, as you realized, it already imposes what you expect. Instead, you must check a property, which says that there's never a comment without a parent thread, in whichever state of your system. Hence, you need (1) a notion of state and (2) to check the property (here: an invariant) on any state.

There are two main ways to design a notion of state:

1. The "global state" approach: you create a State sig (say) that gathers all state variables.
2. The "local state" approach: signatures contain both constant and time-varying fields.

AFAIK, the latter approach is more frequent in Alloy.

Finally, notice Alloy 6 now has features that make it easier to model and specify state-related properties. You can find some information here.