I have this problem below:
That i'am trying to model an Oil-Tank deterministic and i'am using Rodin to simulate this. The thing is that we have an oil-Tank that is level is going to be between 20 and 40 units. And we have an valve that is going to fill in Oil if the level is too low and we have an pump that are going to pump oil if the tank level is too high.
And i have done some refinements but one of the proofs fails and the level is always higher than the high_limit and i have declared a new_value but one of my proof-obligations seems to fail.
And i have tried to change the new_values to irrelevant values and remove the PUMP_RATE or VALVE_RATE but nothing happens and i have tried in -(PUMP_RATE) to -(1000000000000000) or (-1000000000000000) it feels like a dead refined event?
What is wrong here in my Rodin Event?
I can't copy and paste from Rodin so will share a screendump.
