diff --git a/Test/TestMachine.bcm b/Test/TestMachine.bcm index 4c2d8aa20a78779fed3f1bcbe2df81f2d2610020..597d06bf9084bfea3f0924186dc406d4effe50cf 100644 --- a/Test/TestMachine.bcm +++ b/Test/TestMachine.bcm @@ -1,4 +1,12 @@ <?xml version="1.0" encoding="UTF-8" standalone="no"?> <org.eventb.core.scMachineFile org.eventb.core.accurate="true" org.eventb.core.configuration="org.eventb.core.fwd"> - <org.eventb.core.scEvent name="'" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="INITIALISATION" org.eventb.core.source="/Test/TestMachine.bum|org.eventb.core.machineFile#TestMachine|org.eventb.core.event#'"/> + <org.eventb.core.scSeesContext name="'" org.eventb.core.scTarget="/Test/Test.bcc" org.eventb.core.source="/Test/TestMachine.bum|org.eventb.core.machineFile#TestMachine|org.eventb.core.seesContext#*"/> + <org.eventb.core.scInternalContext name="Test"> + <org.eventb.core.scCarrierSet name="Word" org.eventb.core.source="/Test/Test.buc|org.eventb.core.contextFile#Test|org.eventb.core.carrierSet#'" org.eventb.core.type="ℙ(Word)"/> + </org.eventb.core.scInternalContext> + <org.eventb.core.scInvariant name="Tesu" org.eventb.core.label="inv1" org.eventb.core.predicate="name⊆Word" org.eventb.core.source="/Test/TestMachine.bum|org.eventb.core.machineFile#TestMachine|org.eventb.core.invariant#)" org.eventb.core.theorem="false"/> + <org.eventb.core.scVariable name="name" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/Test/TestMachine.bum|org.eventb.core.machineFile#TestMachine|org.eventb.core.variable#(" org.eventb.core.type="ℙ(Word)"/> + <org.eventb.core.scEvent name="namf" org.eventb.core.accurate="false" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="INITIALISATION" org.eventb.core.source="/Test/TestMachine.bum|org.eventb.core.machineFile#TestMachine|org.eventb.core.event#'"> + <org.eventb.core.scAction name="'" org.eventb.core.assignment="name :∣ ⊤" org.eventb.core.label="GEN" org.eventb.core.source="/Test/TestMachine.bum|org.eventb.core.machineFile#TestMachine|org.eventb.core.event#'"/> + </org.eventb.core.scEvent> </org.eventb.core.scMachineFile> diff --git a/Test/TestMachine.bpo b/Test/TestMachine.bpo index 3b2db3235648906c63540a8c63937a7ca3bd0d76..f821d3ff5db06b6306f54e640c911c196713910f 100644 --- a/Test/TestMachine.bpo +++ b/Test/TestMachine.bpo @@ -1,7 +1,16 @@ <?xml version="1.0" encoding="UTF-8" standalone="no"?> -<org.eventb.core.poFile org.eventb.core.poStamp="0"> - <org.eventb.core.poPredicateSet name="CTXHYP" org.eventb.core.poStamp="0"/> - <org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.parentSet="/Test/TestMachine.bpo|org.eventb.core.poFile#TestMachine|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="0"/> - <org.eventb.core.poPredicateSet name="EVTALLHYP'" org.eventb.core.parentSet="/Test/TestMachine.bpo|org.eventb.core.poFile#TestMachine|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="0"/> - <org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/Test/TestMachine.bpo|org.eventb.core.poFile#TestMachine|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="0"/> +<org.eventb.core.poFile org.eventb.core.poStamp="3"> + <org.eventb.core.poPredicateSet name="CTXHYP" org.eventb.core.poStamp="3"> + <org.eventb.core.poIdentifier name="Word" org.eventb.core.type="ℙ(Word)"/> + </org.eventb.core.poPredicateSet> + <org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.parentSet="/Test/TestMachine.bpo|org.eventb.core.poFile#TestMachine|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="3"> + <org.eventb.core.poIdentifier name="name" org.eventb.core.type="ℙ(Word)"/> + </org.eventb.core.poPredicateSet> + <org.eventb.core.poPredicateSet name="EVTIDENTnamf" org.eventb.core.parentSet="/Test/TestMachine.bpo|org.eventb.core.poFile#TestMachine|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="0"> + <org.eventb.core.poIdentifier name="name'" org.eventb.core.type="ℙ(Word)"/> + </org.eventb.core.poPredicateSet> + <org.eventb.core.poPredicateSet name="EVTALLHYPnamf" org.eventb.core.parentSet="/Test/TestMachine.bpo|org.eventb.core.poFile#TestMachine|org.eventb.core.poPredicateSet#EVTIDENTnamf" org.eventb.core.poStamp="0"/> + <org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/Test/TestMachine.bpo|org.eventb.core.poFile#TestMachine|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="3"> + <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="name⊆Word" org.eventb.core.source="/Test/TestMachine.bum|org.eventb.core.machineFile#TestMachine|org.eventb.core.invariant#)"/> + </org.eventb.core.poPredicateSet> </org.eventb.core.poFile> diff --git a/Test/TestMachine.bum b/Test/TestMachine.bum index ae6161f6b34b2e0b9e3f3ecd0333d3d8fadd279a..b6dd03a0d2f4aca636f4c914f496cdccc3e3e311 100644 --- a/Test/TestMachine.bum +++ b/Test/TestMachine.bum @@ -1,4 +1,7 @@ <?xml version="1.0" encoding="UTF-8" standalone="no"?> <org.eventb.core.machineFile org.eventb.core.configuration="org.eventb.core.fwd" version="5"> <org.eventb.core.event name="'" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="INITIALISATION"/> + <org.eventb.core.variable name="(" org.eventb.core.identifier="name"/> + <org.eventb.core.invariant name=")" org.eventb.core.label="inv1" org.eventb.core.predicate="name ⊆ Word"/> + <org.eventb.core.seesContext name="*" org.eventb.core.target="Test"/> </org.eventb.core.machineFile>