vis for psl

From: jguo_at_sei.ecnu.edu.cn
Date: Mon Nov 05 2007 - 18:03:55 MST

• Next message: William Hung: "Root cause of VIS compilation problems is due to flex version differences"
• Previous message: jguo_at_sei.ecnu.edu.cn: "vis for psl"
• Messages sorted by: [ date ] [ thread ] [ subject ] [ author ] [ attachment ]
• Mail actions: [ respond to this message ] [ mail a new topic ]

dear sir,
   recently I download the new VIS wh ich support psl property from PROSYD. I i nstall it and use its commands "sug ar_to_aut " ,"sugar_model_check", then I f ound vis tell me
"sugar_mc error: formula semantic check on desi gn fails:
could not find node corresponding to the name:
                                -ns_light."
I dont know how to find this error . In ctl-model check , once checking the formula error,it will give an counterexample. I donot in psl model che ck if I can get this .now I attached my example for you, could you help me to find error.

I have another question about psl that since vis support psl subset, I donot know psl syntax in vis. if I could get some w rite psl formula rules and some examples about psl modle checking, it should help me und erstand psl in vis.

thanks
GUO Jian

• application/octet-stream attachment: ctlpsl.psl

• application/octet-stream attachment: trafficlight.v

• Next message: William Hung: "Root cause of VIS compilation problems is due to flex version differences"
• Previous message: jguo_at_sei.ecnu.edu.cn: "vis for psl"
• Messages sorted by: [ date ] [ thread ] [ subject ] [ author ] [ attachment ]
• Mail actions: [ respond to this message ] [ mail a new topic ]

This archive was generated by hypermail 2.1.7 : Mon Nov 05 2007 - 18:16:05 MST