#5 maude process is not terminated

[Robert Hein]

This happens on Linux at least. Stopping a proof search does not terminate the maude process as a call of maude.exitValue() after maude.destroy() trows an exception. Also the maude processes can be seen on the process table.

Secondly, after choosing a new system, it is possible that the Maude object is not released somewhere and not treated by garbage collection. Some experiments show that Maude's finalize methode almost never ever get's called and maude processes keep populating the system memory. (this may need some more investigation)

--robert

[Max Schäfer]

Logged In: YES
user_id=1539302
Originator: NO

According to the Java API documentation, the destroy() method _should_ "forcibly terminate" the subprocess, so I'm not sure what's going wrong there...

That the Maude object sticks around, however, is intentional, since it is immediately reused to start a fresh Maude process.