Spinroot

A forum for Spin users

You are not logged in.

#1 2012-03-19 02:08:25

Beth
Member
Registered: 2012-03-19
Posts: 11

"Never Claims"

Hi, 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.

Offline

#2 2012-03-19 04:06:48

spinroot
forum
Registered: 2010-11-18
Posts: 691
Website

Re: "Never Claims"

You can use inline ltl formula, for instance:

ltl p1 { [] <> (a > b) }

Offline

#3 2012-03-24 05:12:50

Beth
Member
Registered: 2012-03-19
Posts: 11

Re: "Never Claims"

Thanks,it worked.

Offline

Board footer

Powered by FluxBB