From: Andrea Fedeli (andrea.fedeli_at_mclink.it)
Date: Thu Nov 06 2008 - 11:55:11 MST
Hi Waseem,
Waseem Muhammad wrote:
> I am using Sugar model checking with VIS and need the VIS supported
> syntax for PSL. VIS CTL syntax is available on web but I can't see one
> for PSL.
I'll leave somebody else more up to date about latest VIS developments
than I am to answer on native PSL support; what I can tell is that some
time ago I had the pleasure to play a bit with a tool that came out of a
FP6 European Project (ProSyD). The Tool was named RAT (Requirement
Analysis Tool) and supported, to some extent, PSL on top of both NuSMV
and VIS.
I am afraid that's not currently maintained, but I've just checked it
can be still downloaded from
http://rat.itc.it/index.php?n=Main.Download
As it was released under LGPL 2.1, it should be possible to take steps
from there...
Cheers,
Andrea.
> I am facing syntax errors while specifying properties with 'next'
> operator, and with brackets and parenthesis.
>
> For instance property
>
> always [{{!LOAD} | {RSTN}} |=> {DSO}];
>
> passes well. But
>
> always {{{!LOAD} | {RSTN}} |=> {DSO}};
>
> gives syntax error.
>
> Does anyone face the same problem?
>
> Regards
> Waseem
>
>
>
-- Andrea Fedeli It is only the great men who are truly obscene. If they had not dared to be obscene, they could never have dared to be great. -- Havelock Ellis
This archive was generated by hypermail 2.1.7 : Thu Nov 06 2008 - 11:57:19 MST