Как смоделировать OIL_TANK
У меня есть эта проблема ниже:
Что я пытаюсь смоделировать детерминистический нефтяной резервуар, и я использую Rodin для моделирования этого. Дело в том, что у нас есть масляный бак, уровень которого будет между 20 и 40 единицами. И у нас есть клапан, который будет заливать масло, если уровень слишком низкий, и у нас есть насос, который будет перекачивать масло, если уровень в резервуаре слишком высок.
И я сделал некоторые уточнения, но одно из доказательств терпит неудачу, и уровень всегда выше, чем high_limit, и я объявил новое_значение, но одно из моих обязательств по доказательству, кажется, терпит неудачу.
И я попытался изменить new_values на нерелевантные значения и удалить PUMP_RATE или VALVE_RATE, но ничего не происходит, и я пробовал в -(PUMP_RATE) на -(10000000000000000) или (-100000000000000000) это похоже на мертвое уточненное событие?
Что не так с моим событием Rodin?
Я не могу копировать и вставлять из Rodin, поэтому поделюсь снимком экрана.
