[Сплав] Ни одного экземпляра не найдено ни одного факта

Question

Я написал следующий код в Alloy. Мне было интересно, почему он не находит экземпляр, поскольку в коде нет никаких фактов.

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 

Answer 1

• Вы не указали объем в вашей команде run
• области дефолта 3 (смысла, вселенная содержит 3 атома каждого сига)
• #Task > 3 не выполним в этой области видимости

Если вы запустили свою оригинальную модель, с многословием, установленным как минимум на «средний», вы должны увидеть что-то подобное в окне консоли с правой стороны

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 

подтверждение того, что возможности для Task был действительно по-умолчанию до 3.

Чтобы устранить эту проблему, указать больший объем, например,

run show for 5