The model checker has the context menu shown only on a single cml file, but this is not intuitive, and is different from the other tools provided in compass.
The menu should be at the project level because a file may contain 0 or many processes but there are no rule stating that the individual file will be self contained e.g. types may be declared in another file.
So it seems like the best solution is to use the same approach for both pog/rttmbt and the model checker.
The model checker has the context menu shown only on a single cml file, but this is not intuitive, and is different from the other tools provided in compass.
The menu should be at the project level because a file may contain 0 or many processes but there are no rule stating that the individual file will be self contained e.g. types may be declared in another file.
So it seems like the best solution is to use the same approach for both pog/rttmbt and the model checker.