Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source
Source file Invar_computation.ml
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303(*******************************************************************************
* electrod - a model finder for relational first-order linear temporal logic
*
* Copyright (C) 2016-2020 ONERA
* Authors: Julien Brunel (ONERA), David Chemouil (ONERA)
*
* This Source Code Form is subject to the terms of the Mozilla Public
* License, v. 2.0. If a copy of the MPL was not distributed with this
* file, You can obtain one at http://mozilla.org/MPL/2.0/.
*
* SPDX-License-Identifier: MPL-2.0
* License-Filename: LICENSE.md
******************************************************************************)openContainerstypegoal_color=|Static_prop|Primed_prop|Invar|Init|Trans|Temporalletto_string(gc:goal_color)=matchgcwith|Static_prop->"Static_prop"|Primed_prop->"Primed_prop"|Invar->"Invar"|Init->"Init"|Trans->"Trans"|Temporal->"Temporal"letppoutgc=Fmtc.(pfout"%a"(styled`Yellowstring)(to_stringgc))(* Computes the most general color between two colors *)letmax_colorc1c2=match(c1,c2)with|Static_prop,Static_prop->Static_prop|(Init|Static_prop),(Init|Static_prop)->Init|(Primed_prop|Init|Static_prop),(Primed_prop|Init|Static_prop)->Primed_prop|(Invar|Static_prop),(Invar|Static_prop)->Invar|(Trans|Static_prop),(Trans|Static_prop)->Trans|_,_->Temporal(* same as max_color, but without Invar nor Trans *)letmax_color_wiwtc1c2=match(c1,c2)with|Static_prop,Static_prop->Static_prop|(Init|Static_prop),(Init|Static_prop)->Init|(Primed_prop|Init|Static_prop),(Primed_prop|Init|Static_prop)->Primed_prop|_,_->Temporalletrecremove_always_from_invar(Elo.Fml{node;_}asfml)=letopenEloinmatchnodewith|LUn(G,subfml)->remove_always_from_invarsubfml|LBin(fml1,And,fml2)->letfml1'=remove_always_from_invarfml1inletfml2'=remove_always_from_invarfml2inlbinaryfml1'and_fml2'|_->fmlletadd_always_to_invar(Elo.Fml{node;_}asfml)=letopenEloinmatchnodewithLUn(G,_)->fml|_->lunaryalwaysfmlletis_const(elo:Elo.t)(name:Name.t)=assert(Domain.memnameelo.Elo.domain);Domain.get_exnnameelo.Elo.domain|>Relation.is_constclass['self]computer(elo:Elo.t)=object(_:'self)inherit['self]Elo.foldmethodbuild_fml()f'_=f'methodbuild_Run()blk'=List.fold_leftmax_color_wiwtStatic_propblk'methodbuild_Check()blk'=List.fold_leftmax_color_wiwtStatic_propblk'methodbuild_True()=Static_propmethodbuild_False()=Static_propmethodbuild_Block()blk_colors=List.fold_leftmax_colorStatic_propblk_colorsmethodbuild_FIte()fte=match(f,t,e)with|Static_prop,Static_prop,Static_prop->Static_prop|(Init|Static_prop),(Init|Static_prop),(Init|Static_prop)->Init|((Primed_prop|Init|Static_prop),(Primed_prop|Init|Static_prop),(Primed_prop|Init|Static_prop))->Primed_prop|_,_,_->Temporalmethodbuild_Let()__bs'__block'=assertfalse(* SIMPLIFIED *)(* quant *)methodbuild_Quant()quant'(_,_,range_color)blk_colors=letblk_color=List.fold_leftmax_color_wiwtStatic_propblk_colorsinletsim_binding_color=max_color_wiwtStatic_proprange_colorinquant'sim_binding_colorblk_colormethodbuild_All()=max_colormethodbuild_No()=max_colormethodbuild_Some_()=max_color(* lbinop *)methodbuild_LBin()f1'op'f2'=op'f1'f2'methodbuild_And()=max_colormethodbuild_Iff()=max_color_wiwtmethodbuild_Imp()=max_color_wiwtmethodbuild_U()__=Temporalmethodbuild_Or()=max_color_wiwtmethodbuild_R()__=Temporalmethodbuild_S()__=Temporalmethodbuild_T()__=Temporal(* lunop *)methodbuild_LUn()op'f'=op'f'methodbuild_X()f'=matchf'withStatic_prop|Init->Primed_prop|_->Temporalmethodbuild_F()_=Temporalmethodbuild_G()f'=matchf'with|Init|Static_prop|Invar->Invar|Primed_prop|Trans->Trans|_->Temporalmethodbuild_H()_=Temporalmethodbuild_O()_=Temporalmethodbuild_P()_=Temporalmethodbuild_Not()f'=max_color_wiwtStatic_propf'(* compo_op *)methodbuild_RComp()f1'op'f2'=op'f1'f2'methodbuild_REq()=max_color_wiwtmethodbuild_In()=max_color_wiwtmethodbuild_NotIn()=max_color_wiwtmethodbuild_RNEq()=max_color_wiwt(* icomp_op *)methodbuild_IComp()e1'op'e2'=op'e1'e2'methodbuild_Gt()=max_color_wiwtmethodbuild_Gte()=max_color_wiwtmethodbuild_IEq()=max_color_wiwtmethodbuild_INEq()=max_color_wiwtmethodbuild_Lt()=max_color_wiwtmethodbuild_Lte()=max_color_wiwt(************************** exp ********************************)methodbuild_exp()pe'__=pe'methodbuild_oexp()color_=colormethodbuild_Compr()sbs'b'=letblk_color=List.fold_leftmax_color_wiwtStatic_propb'inletmax_color_for_simbindings(color_acc:goal_color)((__disj1,__vars1,e1):bool*int*goal_color)=max_color_wiwtcolor_acce1inletsim_bindings_color=List.fold_leftmax_color_for_simbindingsStatic_propsbs'inmax_color_wiwtsim_bindings_colorblk_colormethodbuild_Iden()=Static_propmethodbuild_Name()r=ifis_constelorthenStatic_propelseInitmethodbuild_Var()__id=Static_propmethodbuild_None_()=Static_propmethodbuild_Univ()=Static_propmethodbuild_Prime()f'=matchf'withStatic_prop|Init->Primed_prop|_->Temporalmethodbuild_RIte()f't'e'=match(f',t',e')with|Static_prop,Static_prop,Static_prop->Static_prop|(Init|Static_prop),(Init|Static_prop),(Init|Static_prop)->Init|((Primed_prop|Init|Static_prop),(Primed_prop|Init|Static_prop),(Primed_prop|Init|Static_prop))->Primed_prop|_,_,_->Temporal(* rbinop *)methodbuild_RBin()f1'op'f2'=op'f1'f2'methodbuild_Union()=max_color_wiwtmethodbuild_Inter()=max_color_wiwtmethodbuild_Join()=max_color_wiwtmethodbuild_LProj()=max_color_wiwtmethodbuild_Prod()=max_color_wiwtmethodbuild_RProj()=max_color_wiwtmethodbuild_Diff()=max_color_wiwtmethodbuild_Over()=max_color_wiwt(* runop *)methodbuild_RUn()op'e'=op'e'methodbuild_RTClos()=Fun.idmethodbuild_Transpose()=Fun.idmethodbuild_TClos()=Fun.id(*********************************** iexp **************************************)methodbuild_iexp()iexp'_=iexp'methodbuild_IBin()i1'op'i2'=op'i1'i2'methodbuild_IUn()op'i'=op'i'methodbuild_Num()_=Static_propmethodbuild_Add()=max_color_wiwtmethodbuild_Neg()=max_color_wiwtStatic_propmethodbuild_Sub()=max_color_wiwtmethodbuild_Card()r'=r'end(* Computes the color (Invar, Static_prop, Init or Temporal) of an
elo formula *)letcoloreloelo_fml=(newcomputerelo)#visit_fml()elo_fml