Date: Mon Nov 05 2007 - 18:03:55 MST
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:
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.
This archive was generated by hypermail 2.1.7 : Mon Nov 05 2007 - 18:16:05 MST