An experimental framework for temporal verification based on first-order linear-time temporal logic. Our goal is to express transition systems in first-order logic and verify temporal correctness properties, including safety and liveness.
When running with --time, previously we would calculate the "non-solver" time by taking the total end-to-end time and subtracting the solver time. This isn't accurate when the solver is called concurrently.
This PR directly uses the getrusage system call to get time spent in the process, excluding children. This isn't quite the same as real time (it excludes time spent in other processes for example), but it much better accounts for concurrency. It's the same thing that the Linux time utility would report. (Actually I wanted to know how time worked so I read the source code and that's how I discovered this syscall in the first place.)
When running with
--time, previously we would calculate the "non-solver" time by taking the total end-to-end time and subtracting the solver time. This isn't accurate when the solver is called concurrently.This PR directly uses the
getrusagesystem call to get time spent in the process, excluding children. This isn't quite the same as real time (it excludes time spent in other processes for example), but it much better accounts for concurrency. It's the same thing that the Linuxtimeutility would report. (Actually I wanted to know howtimeworked so I read the source code and that's how I discovered this syscall in the first place.)