From: Thomas M. <tho...@sy...> - 2012-10-02 13:03:52
|
Hi Ulyana, Thanks for your message, and having sent the log and your configuration file. > Here is what I can observe now: > I have 3 contexts, 8 machines and 1 composition machine in my project. > Only 1 context and 2 machines have their proof obligation lists > available. These are also only components that have corresponding .bps > and .bpo files (I don't know their purpose, I just observe this). > Project cleaning doesn't change anything! Here are some details for your information, even if it's not very relevant to know that from the user side : .bps are "B" "P"roof "S"tatus files they give a summary of what is proved and what isn't They exist so that there is no need to load the "B" "PR"oof files (.bpr) that can be huge, to get this info. .bpo stand for "B" "P"roof "O"bligation files. .bum file extension stands for "B" "U"nchecked "M"achine, ".buc" for "B" "U"nchecked "C"ontext. .bcm file extension stands for "B" "C"hecked "M"achine, ".buc" for "B" "C"hecked "C"ontext (in sense of statically checked). You don't see .bpo and .bps files for some components which to me significates that the builder did not finish his job on your project. However, I did not get confirmation of this from reading your log, as there is no error involving the builder itself. There is a bug in the Event-B Explorer View that fails with the Composed Machine you use. But it takes place in a "safe" zone, and shall not influence the builder. The option "build automatically" is still enabled when you clean your project, or? Could you please try to rename the extension of the composed machine for example with the suffix _bckp and clean/refresh your project. You could then tell me if it allows the builder to finish his job. Best regards, Thomas -- ------------------------------------------------------------------------ Thomas MULLER Tél. : (+33)(0)4 42 90 65 66 Engineer in Formal Methods SYSTEREL ------------------------------------------------------------------------ Standard / Fax : (+33)(0)4 42 90 41 20 / 29 site : www.systerel.fr ------------------------------------------------------------------------ |