Анализатор сплавов не находит примеры, которые были найдены до применения предиката с ограничением мощности - PullRequest
Новая
       8

Анализатор сплавов не находит примеры, которые были найдены до применения предиката с ограничением мощности

0 голосов
/ 11 января 2019

Я играл со сплавом, пытаясь построить модель, представляющую шаги, которые пользователь мог бы выполнить при заполнении формы мастера. Я пытался смоделировать его шаги, используя график, который связан и всегда имеет путь к последнему шагу.

После создания исходной модели я хотел увидеть примеры структуры, в которой было более 3 дуг, соединяющих узлы.

Оказывается, что если я использую пустой предикат, выполняю и смотрю на найденные экземпляры, я могу найти тот, который имеет более 3 дуг. Но когда я прямо спрашиваю об этом в предикате, сплав говорит мне: No instance found: 

pred example (f: Flow) {
  #f.paths > 3
}

Я неправильно использую оператор кардинальности?

Вся модель ниже: 

sig FlowObject {}

sig Flow {
  steps: set FlowObject,
  initial_step: steps,
  final_step: steps,
  paths: (steps - final_step)->(steps - initial_step),
} {
  // The final step is reachable from every step
  all s: (steps - final_step) | final_step in s.^paths
  // Every step is reachable from the initial step
  all s: (steps - initial_step) | s in initial_step.^paths
  // There are no loops
  no iden & paths
}

// No FlowObject is shared between Flows
fact {
  all f1, f2: Flow | f1 != f2 => no f1.steps & f2.steps
}

pred example (f: Flow) {
  // It finds this example if I remove this predicate
  #f.paths > 3
}

run example for 5 but 1 Flow
...