2012-03-24T04:12:50ZFluxBBhttp://spinroot.com/fluxbb/viewtopic.php?id=788Thanks,it worked.]]>http://spinroot.com/fluxbb/profile.php?id=62102012-03-24T04:12:50Zhttp://spinroot.com/fluxbb/viewtopic.php?pid=1621#p1621You can use inline ltl formula, for instance:
ltl p1 { [] <> (a > b) }
]]>http://spinroot.com/fluxbb/profile.php?id=22012-03-19T03:06:48Zhttp://spinroot.com/fluxbb/viewtopic.php?pid=1609#p1609Hi, i just started using iSPIN for the implementation of my project. Quick question, where should i place the Never Claims generated from LTL formulas??? Should it be within a process in my model or outside the process?? any assistance on the above matter will be highly appreciated.]]>http://spinroot.com/fluxbb/profile.php?id=62102012-03-19T01:08:25Zhttp://spinroot.com/fluxbb/viewtopic.php?pid=1608#p1608