modelingalloy

Alloy: unexpected instance, difference between Sig'=Sig & Sig.field' = Sig.field

I am trying to model the following properties:

I have modelled it like so:

var sig Rule {}
var sig Disabled in Rule {}
sig Observable {}

var one sig State {
    var raised: Rule -> lone Observable
}

pred stutter {
    State' = State
}

pred raiseAlert[r: Rule, p: Observable] {
    // rule must not be disabled
    r not in Disabled
    (r -> p) not in State.raised
    State.raised' = State.raised + (r -> p)
    Rule' = Rule
}

pred muteRule[r: Rule] {
    // not yet in Disabled
    r not in Disabled
    Disabled' = Disabled + r
    // State.raised' = State.raised // this results in "No instance found" ?
    State' = State
}

pred liveness {
     (some r: Rule, p: Observable | raiseAlert[r, p])
    or (some r: Rule | muteRule[r])
}

fact next {
    always (liveness)
}

run liveness

Two questions:

  1. Here, in State 1 somehow we end up we less "raised" than in State 0. However, I only ever specified how to add more raised alerts, never how to remove them. How is this possible? enter image description here
  1. What's the difference between "State' = State" and State.raised' = State.raised? Replacing the first with the second, results in No Instance found, and I don't understand why?

EDIT:

var sig Rule {}
var sig Disabled in Rule {}
sig Observable {}

var one sig State {
    var raised: Rule -> lone Observable
}
fact {
    some Rule
    some Observable
}
pred stutter {
    State' = State
    State.raised' = State.raised
    Disabled' = Disabled
    Rule' = Rule
}

pred raiseAlert[r: Rule, p: Observable] {
    r not in Disabled
    (r -> p) not in State.raised
    State.raised' = State.raised + (r -> p)
    Rule' = Rule
    State' = State
    Disabled' = Disabled
}

pred muteRule[r: Rule] {
    r not in Disabled
    Disabled' = Disabled + r
    State' = State
    // remove those elements from raised which start with rule "r"
    State.raised' = State.raised - (r <: State.raised)
}

pred liveness_only_stutter {
    always ((some r: Rule, p: Observable | raiseAlert[r, p])
        or (some r: Rule | muteRule[r]) or stutter)
}

pred liveness_no_instances {
    always ((some r: Rule, p: Observable | raiseAlert[r, p])
        or (some r: Rule | muteRule[r]))
}

pred liveness_actually_interesting {
    // this one actually generates interesting instances
    (some r: Rule, p: Observable | raiseAlert[r, p])
        or (some r: Rule | muteRule[r])
}


run liveness_actually_interesting

After this edit:

Solution

  • Many comments are in order. First, I wouldn't call liveness the predicate representing possible traces. Usually we keep liveness for liveness properties we want to check, not properties we want to take as a fact.

    With next as a fact, it doesn't seem really useful to run liveness, run {} will do.

    Then, you have a stutter predicate but you don't say that this may happen as an event in the next fact.

    Also notice, but maybe that was clear to you, that State may take various values among a finite number of values defined by the scope. The one attribute only says that it has exactly one value in every instant.

    In next you allow muteRule to happen, and this event doesn't constrain raised. So, as explained just before, raised may change arbitrarily, which is what happens in your question 1.

    Re question 2, if you have no instance for a run, it's because you have over-constrained your model. So you must look again at all constraints and think about how they may interact. In particular, they may interact by preventing the existence of any trace or by only allowing finite traces. But Alloy only considers infinite traces as instances (this is one reason to systematically add a stutter event in the next fact).

    Now, assessing how events interact in your model is a bit hard because, as explained above, you haven't said what happens to every variable in every event (some frame conditions are missing). In raiseAlert for instance, anything may happen to Disabled, to State, and to raised on values other than State. So for instance, raiseAlert may increase the value of State.raised but decrease it for other states at the same time. Similarly for muteRule.

    Please fix your model first, by stating explicitly what happens to every variable.

    EDIT: Now that your model is edited, some comments.

    Regarding "liveness", I was just pointing out that the name was badly chosen. But you can (and usually should) still define the predicate contents in a fact stating what are the possible traces, like this:

    fact possible_traces {
always ((some r: Rule, p: Observable | raiseAlert[r, p])
        or (some r: Rule | muteRule[r]) or stutter)
}

    Second, note that in your events, you only modify raised on State. Which means you allow raised to change for every other state value. I don't think this is what you mean in general. One way to say that raised changes only on State is rather to write:

    raised' = raised - State -> r -> univ

    This way, you effectively specify what happens to every tuple in raised.

    Also you forgot to say what happens to Rule in muteRule.

    Re the fact that you don't always get interesting instances, that's normal. Your system is now allowed to stutter, which is good in general, but a consequence is that you may also get "uninteresting" instances. But these are correct instances! To see other instances, you may use the New ... buttons in the Visualizer; you could also issue specific run commands; and you could finally (but that will need a bit more experience) add so-called "weak fairness" properties (which somehow force progress when it's possible).

    Finally, regarding the question on traces. I was supposing you knew about that as you're using the var keyword which isn't Daniel Jackson's book either. This is specific to Alloy 6: please refer to Formal Software Design with Alloy 6 for a tutorial-style on-going book.