Go2Pins now accepts a second argument, a formula to run directly modelchecking on it. * main.go : Here.