-
Following to a post from Matthias, there are several inference rules that are ill-defined in both the Rodin wiki and the event-B prover. The usage of these rules can introduce inconsistency in the prover (e.g., allow one to prove false which is invalid, as Matthias did).
Some rules already known to be ill-defined are MH, HM, FORALL_INST_MP and FIN_SUBSETEQ_R.
These rules should be fixed in...
2009-11-10 21:55:29 UTC by lvoisin
-
The latest release of the renaming/refactory plug-in (v0.0.4) allows the renaming of machines and contexts and the respective propagation over the related files. More information can be found here: http://wiki.event-b.org/index.php/Refactoring_Framework. Instead of using the "rename" option, use instead the "refactory" option also provided by right clicking on it. The refactory plug-in uses the...
2009-11-10 10:44:06 UTC by renato_silva
-
I have made a collection of axioms about the integers.
It is well-known that those axioms characterize the integers up to isomorphism (modulo some technicalities due to Gödel).
Hence these axioms characterize the integers as good as the Peano axioms characterize the natural numbers.
Some of the axioms (stated as Rodin theorems) in the attached file can be proved. Some can only be proved...
2009-11-09 17:17:25 UTC by wohuai
-
When I create a context named "axioms", Camille gives an error message:
Expected: Identifier literal.
2009-11-09 15:39:42 UTC by wohuai
-
fuersta committed revision 7777 to the RODIN SVN repository, changing 14 files.
2009-11-09 13:02:15 UTC by fuersta
-
fuersta committed revision 7776 to the RODIN SVN repository, changing 6 files.
2009-11-09 10:28:03 UTC by fuersta
-
I just create a sample project in new rodin platform version 1.1
I get a singular error when creating a context and trying to use it by a machine.
the sample project is joined
the following error is showed : "context ctx0 does not have a configuration".
2009-11-07 11:06:40 UTC by smn_
-
nicolas_beauger committed revision 7775 to the RODIN SVN repository, changing 3 files.
2009-11-06 17:10:51 UTC by nicolas_beauger
-
If a machine has a variable and an event with the same name, the refinement of that machine cannot be opened with Camille. It can be opened with the structural editor.
The following Stacktrace is shown (in the Editor window):
java.lang.ArrayStoreException
at org.eclipse.emf.common.util.BasicEList.assign(BasicEList.java:191)
at...
2009-11-06 16:14:25 UTC by jastram
-
nicolas_beauger committed revision 7774 to the RODIN SVN repository, changing 3 files.
2009-11-06 15:31:47 UTC by nicolas_beauger
