Hi Christian,
I re installed mCRL2. Now on checking constraint in the Validation window, I got the below error:
pbes2bool produced no output.
pbes2bool produced no output.
and also the below error on executing the examples given in the eclipse henshin tutorial.
lps2pbes returned exit code 1:
[12:08:17 error] basic or defined sort Fork is not declared
[12:08:17 error] could not type check modal formula TEMPORARILY IN ATERM FORMATStateMust(RegTransOrNil(ActTrue),StateForall([DataVarId(f1,SortId(Fork)),DataVarId(f2,SortId(Fork))],StateExists([DataVarId(p,SortId(Philosopher))],StateMust(RegSeq(UntypedActMultAct([UntypedAction(left,[UntypedIdentifier(p),UntypedIdentifier(f1)])]),UntypedActMultAct([UntypedAction(right,[UntypedIdentifier(p),UntypedIdentifier(f2)])])),StateNu(X,[],StateMu(Y,[],StateAnd(StateMust(UntypedActMultAct([UntypedAction(release,[UntypedIdentifier(p),UntypedIdentifier(f1),UntypedIdentifier(f2)])]),StateVar(X,[])),StateMust(ActNot(UntypedActMultAct([UntypedAction(release,[UntypedIdentifier(p),UntypedIdentifier(f1),UntypedIdentifier(f2)])])),StateVar(Y,[])))))))))
lps2pbes returned exit code 1:
[12:08:17 error] basic or defined sort Fork is not declared
[12:08:17 error] could not type check modal formula TEMPORARILY IN ATERM FORMATStateMust(RegTransOrNil(ActTrue),StateForall([DataVarId(f1,SortId(Fork)),DataVarId(f2,SortId(Fork))],StateExists([DataVarId(p,SortId(Philosopher))],StateMust(RegSeq(UntypedActMultAct([UntypedAction(left,[UntypedIdentifier(p),UntypedIdentifier(f1)])]),UntypedActMultAct([UntypedAction(right,[UntypedIdentifier(p),UntypedIdentifier(f2)])])),StateNu(X,[],StateMu(Y,[],StateAnd(StateMust(UntypedActMultAct([UntypedAction(release,[UntypedIdentifier(p),UntypedIdentifier(f1),UntypedIdentifier(f2)])]),StateVar(X,[])),StateMust(ActNot(UntypedActMultAct([UntypedAction(release,[UntypedIdentifier(p),UntypedIdentifier(f1),UntypedIdentifier(f2)])])),StateVar(Y,[])))))))))
Many thanks