context PedalFreio inv: pedalDuro not Hidrovacuo.taRegular or not CilindroMestre.taRegular or Hidrovacuo.TubulacaoFreio.taObstruida implies self.taDuro context PedalFreio inv: pedalFundo not SistemaFreio.CilindroMestre.taRegular or SistemaFreio.taVazando or SistemaFreio.arNoSistema implies self.taFundo context PedalFreio inv: pedalBaixo SistemaFreio.Pastilha.condicao = desgastada or SistemaFreio.LonasDeFreio.taDesgastada or SistemaFreio.LonasDeFreio.taDesregulada or not Hidrovacuo.taRegular or SistemaFreio.arNoSistema or SistemaFreio.taVazando implies self.funcionamento = baixo context PedalFreio inv: pedalTrepidando Tambor.condicao = ovalisado or Pastilha.condicao = desgastada or not Hidrovacuo.TubulacaoFreio.DiscoFreio.taRegular or SistemaFreio.DiscoFreio.CuboDeRoda.taEmpenado implies self.taTrepidando context PedalFreio inv: pedalMacio SistemaFreio.arNoSistema implies self.funcionamento = macio context PedalFreio inv: frouxo not self.bemFixado implies self.funcionamento = frouxo context Pastilha inv: pastilhaDesgastada SistemaFreio.GuiaFreioDisco.taEmperrada implies self.condicao = desgastada context Hidrovacuo inv: hidrovacuoIrregular SistemaFreio.OleoFreio.taContaminado or SistemaFreio.OleoFreio.taSaturado or SistemaFreio.CilindroMestre.taVazando or TubulacaoFreio.taVazando or TubulacaoFreio.taObstruida implies not self.taRegular context CilindroMestre inv: cilindroMestreIrregular SistemaFreio.OleoFreio.taContaminado or SistemaFreio.OleoFreio.taSaturado implies not self.taRegular context TubulacaoFreio inv: tubulacaoObstruida SistemaFreio.OleoFreio.taContaminado or not self.taAssentada or self.taDeformada implies self.taObstruida context Lanterna inv: lanternaSempreAcesa not Carro.SistemaFreio.PedalFreio.Interruptor.taRegular and self.Tipo = pedalFreio implies self.sempreAcesa context Lanterna inv: lanternaNaoAcende not Carro.SistemaFreio.PedalFreio.Interruptor.taRegular and self.Tipo = pedalFreio implies not self.acende context LuzFreioPainel inv: luzFreioPainelAcesa Painel.Carro.SistemaFreio.Pastilha.condicao = desgastada or Painel.Carro.SistemaFreio.taVazando or Painel.Carro.SistemaFreio.FreioDeMao.taAcionado or not Painel.Carro.SistemaFreio.PedalFreio.Interruptor.taRegular implies self.taAcesa context SistemaFreio inv: freioIneficiente Pastilha.condicao = vitrificada or self.pressaoBaixa or Tambor.condicao = ovalisado or OleoFreio.ta_contaminado or self.arNoSistema or not CilindroMestre.taRegular or self.taVazando implies self.falhasFreio = ineficiente context Motor inv: rotacaoOscilando not Carro.SistemaFreio.Hidrovacuo.taRegular implies self.rotacaoOscilando context Hidrovacuo inv: hidrovacuoChiando not self.taRegular implies self.taChiando context SistemaFreio inv: pressaoBaixa not Hidrovacuo.taRegular or not CilindroMestre.taRegular or not PedalFreio.taRegulado or TubulacaoFreio.taVazando implies self.pressaoBaixa context SistemaFreio inv: freadaBrusca not Hidrocacuo.taRegular or TubulacaoFreio.taObstruida or not CilindroMestre.taRegular or not Tambor.LonasDeFreio.taRegulada implies self.falhasFreio = freadaBrusca context OleoFreio inv: baixoNivelOleo SistemaFreio.pastilha.condicao = desgastada or SistemaFreio.taVazando implies self.nivel = baixo context Pastilha inv: pastilhaChiando self.condicao = desgastada or self.condicao = vitrificada implies self.taChiando context Tambor inv: barulhoAcionamentoSapatas self.condicao = ovalisado implies self.barulhoSapatas context Tambor inv: tamborChiando self.condicao = ovalisado or not self.taAssentado implies self.taChiando context Roda inv: rodaEmperrada Carro.SistemaFreio.Tambor.condicao = ovalisado or Carro.SistemaFreio.TubulacaoFreio.taObstruida or not Carro.SistemaFreio.Tambor.taAssentado or GuiaFreioDisco.taEmperrada or not CilindroMestre.taRegular implies self.taEmperrada context Carro inv: carroPuxa SistemaFreio.TubulacaoFreio.taObstruida implies Carro.carroPuxa context SistemaFreio inv: arNoSistema OleoFreio.taSaturado or not self.sangriaRealizadaCorretamente implies self.arNoSistema context SistemaFreio inv: semFreio self.taVazando or self.arNoSistema implies self.falhasFreio = semFreio context SistemaFreio inv: vazamento CilindroMestre.taVazando or CilindroRoda.taVazando or TubulacaoFreio.taVazando implies self.taVazando context Tambor inv: tamborNaoAssentado SistemaFreio.Carro.Roda.trocaRecente implies not self.taAssentado context Roda inv: rodaSuperaquecida self.taEmperrada implies self.taSuperaquecida context Roda inv: rodaDianteiraChiando Carro.SistemaFreio.Pastilha.taChiando or Carro.SistemaFreio.Hidrovacuo.taChiando implies self.taChiandoDianteira context Roda inv: rodaTraseiraChiando Carro.SistemaFreio.Tambor.taChiando implies self.taChiandoTraseira context Roda inv: rodaChiandoAoFrear self.taChiandoTraseira or self.taChiandoDianteira implies self.taChiando context Interruptor inv: interruptorIrregular PedalFreio.SistemaFreio.Carro.SistemaEletrico.defeito implies not self.taRegular --Restricoes context PedalFreio inv: restricao self.funcionamento = macio xor self.funcionamento = normal implies self.funcionamento <> baixo context PedalFreio inv: restricao self.funcionamento = macio xor self.funcionamento = baixo implos self.funcionamento <> normal context PedalFreio inv: restricao self.funcionamento = normal xor self.funcionamento = baixo implies self.funcionamento <> macio context PedalFreio inv: restricao self.taTrepidando or self.taFundo or not self.taRegulado or not self.bemFixado or taDuro implies self.funcionamento <> normal context Tambor inv: restricao self.taChiando or self.barulhoSapatas or not self.taAssentado implies self.condicao <> normal context Tambor inv: restricao self.condicao = ovalisado implies self.condicao <> normal context Tambor inv: restricao self.condicao = normal implies self.condicao <> ovalisado context Pastilha inv: restricao self.condicao = desgastada xor self.condicao = vitrificada implies self.condicao <> normal context Pastilha inv: restricao self.condicao = desgastada xor self.condicao normal implies self.condicao <> vitrificada context Pastilha inv: restricao self.condicao = vitrificada xor self.condicao normal implies self.condicao <> desgastada context Pastilha inv: restricao self.taChiando implies self.condicao <> normal context Pastilha inv: restricao self.condicao = normal implies not self.taChiando context Interruptor inv: restricao self.tipo = pedalFreio implies self.tipo <> freioDeMao context Interruptor inv: restricao self.tipo = freioDeMao implies self.tipo <> pedalFreio context SistemaFreio inv: restricao self.falhasFreio = semFreio xor self.falhasFreio = normal xor self.falhasFreio = ineficiente implies self.falhasFreio <> freiadaBrusca context SistemaFreio inv: restricao self.falhasFreio = semFreio xor self.falhasFreio = normal xor self.falhasFreio = freiadaBrusca implies self.falhasFreio <> ineficiente context SistemaFreio inv: restricao self.falhasFreio = semFreio xor self.falhasFreio = freiadaBrusca xor self.falhasFreio = ineficiente implies self.falhasFreio <> normal context SistemaFreio inv: restricao self.falhasFreio = freiadaBrusca xor self.falhasFreio = ineficiente self.falhasFreio = normal implies self.falhasFreio <> semFreio context SistemaFreio inv: restricao self.arNoSistema or self.taVazando or self.pressaoBaixa or not self.sangriaRealizadaCorretamente implies self.falhasFreio <> normal