I'm using SPIN Model Checker, I'd like to know If SPIN is a close box or not. Can be used passing parameters from an upper level (ex: Phyton or batch?). I'm interested on Simulation mode of SPIN, not on the Verification mode.
In the end, I'd like to know If (always in simulation mode) there is any method to write the simulation output to a phisical File, without using C embedded code.
Been working with spin for years and haven't heard of any way to pass arguments into a promela program.
As far as the output, you can easily pipe the output of spin to a file, e.g. spin model.pml > myfile.txt