CODEWITHSUNDEEP
instancealloy
user1315621
user1315621

Reputation: 3412

[Alloy]No instance found with no fact

I wrote the following code in Alloy. I was wondering why it doesn't find an instance since there are no facts at all in code. 

abstract sig TaskStatus {}
one sig Completed extends TaskStatus {}
one sig Waiting extends TaskStatus {}
one sig OnGoing extends TaskStatus {}

sig Capability {}

sig Task {
    status: one TaskStatus,
    precondition: set Task,
    capability: one Capability
}

sig Agent {
    tasks: set Task,
    capabilities: set Capability
}

sig ToDoList {
    tasks: set Task
}


pred show {
    some Capability
    some Agent
    some ToDoList
    #Task > 3
}
run show

Upvotes: 0

Views: 115

Answers (1)

Aleksandar Milicevic
Aleksandar Milicevic

Reputation: 3867

  • You didn't specify a scope in your run command
  • the scope defaulted to 3 (meaning, the universe contains 3 atoms of every sig)
  • #Task > 3 is not satisfiable in that scope

If you run your original model, with verbosity set at least to "medium", you should see something like this in the console window on the right-hand side

Executing "Run show"
Sig this/Completed scope <= 1
Sig this/Waiting scope <= 1
Sig this/OnGoing scope <= 1
Sig this/TaskStatus scope <= 3
Sig this/Capability scope <= 3
Sig this/Task scope <= 3
Sig this/Agent scope <= 3
Sig this/ToDoList scope <= 3

confirming that the scope for Task was indeed by default set to 3.

To fix the problem, specify a larger scope, e.g., 

run show for 5

Upvotes: 1

Related Questions