From ca39d28b64fe0925f2f83fd8ca44591dff366100 Mon Sep 17 00:00:00 2001 From: CoderiGenius <29704758+CoderiGenius@users.noreply.github.com> Date: Tue, 29 Dec 2020 20:09:51 +0000 Subject: [PATCH] add test --- Test/TestMachine.bcm | 10 +++++++++- Test/TestMachine.bpo | 19 ++++++++++++++----- Test/TestMachine.bum | 3 +++ 3 files changed, 26 insertions(+), 6 deletions(-) diff --git a/Test/TestMachine.bcm b/Test/TestMachine.bcm index 4c2d8aa..597d06b 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 3b2db32..f821d3f 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 ae6161f..b6dd03a 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> -- GitLab