Beweren en bewijzen/2010-11/oefenpagina/bedrading
| literatuur |
Hier bouwen we samen een bibliotheek van specificaties van elektrische apparaten in propositielogica op. Deze specificaties kun je gebruiken in de uitwerking van diverse studietaken. Klik bovenaan op Bewerken, kijk hoe het Sjabloon BenB/Specificatie gebruikt is in het eerste voorbeeld en voeg een voorbeeld toe of breid een bestaand voorbeeld uit.
- Voorwaarde vooraf
- Je hebt de opgegeven literatuur gelezen.
- Opdracht
- Voeg een apparaat toe of breid de specificatie van een apparaat uit of verbeter een fout. Zet je naam dan bij het lijstje van auteurs van het apparaat.
- Regel
- Propositielogica is een zeer eenvoudige taal zonder middelen voor renaming, identification en hiding. Alle namen moeten daarom over het hele systeem uniek zijn. Dit kun je bereiken door de namen te laten beginnen met de afkorting van de naam van het bewuste ding.
- Spanningsveld
- Als namen zo kort zijn dat de formules overzichtelijk blijven, kan men hun betekenis moeilijk onthouden. Betekenisvolle namen zijn langer, en daardoor worden de formules onoverzichtelijker.
- Domeinmodel
- Voor deze opdracht voldoet bij de naam van elke propositie een korte bewering in natuurlijke taal: wat moet in het echt gelden, wil deze propositie waar zijn?
- Specificatie
- Een leesbaar opgemaakte formule in syntactisch correcte propositielogica alsmede een vertaling naar helder Nederlands. Het e.e.a. met inachtneming van de bekende kwaliteitscriteria.
- Commentaren
- Als je commentaar geeft op eerdere uitwerkingen, doe dit op deze manier:
{{!|~~~||JE COMMENTAAR}} - Fout in de MediaWiki-software
- Bij deze opdracht werken de edit-links per sectie niet. Je moet altijd de hele pagina editen.
| [[Image:Gerdriaan Mulder .jpg|right|60px|nothumb|]] | ||
| Gerdriaan Mulder → Beweren en bewijzen | Remove this comment when resolved! | |
| Ik kom terug op bovenstaande bewering. De edit-knop linkt inderdaad naar de editpagina van de template. Een workaround kan zijn door de gebruikers zelf een sectie te laten maken met de naam van het artefact en daaronder de template te gebruiken. Dan kan de sectie-definitie uit de template, en daarbij de __ NOEDITSECTION __, want die definitie geldt voor de gehele pagina en niet slechts voor 1 sectie. | [[Image:Gerdriaan Mulder .jpg|right|60px|nothumb|]] | |
| Gerdriaan Mulder → Beweren en bewijzen | Remove this comment when resolved! | |
Inhoud
- 1 cd-speler
- 2 box links
- 3 Synthesizer
- 4 box rechts
- 5 Subwoofer
- 6 waterkoker
- 7 Elektrisch Fornuis
- 8 Magnetron
- 9 Bureaulamp
- 10 Koelkast
- 11 Boormachine
- 12 Lichtsensor
- 13 Strijkijzer
- 14 Tosti-ijzer
- 15 Electrische tandenborstel
- 16 draadloze telefoon
- 17 televisie
- 18 DVD-speler
- 19 TV (focus op AV voor bijv, een dvd speler)
- 20 versterker
- 21 Koffiezetapparaat
- 22 Rookmelder
- 23 Stekkerdoos
- 24 Zwart/wit printer
- 25 Thermostaat
- 26 garagedeur bediening
- 27 elektrische gitaar met solide body
- 28 Elektrische Tandenborstel
- 29 mediacenter
- 30 Ventilator (2 standen)
- 31 Wekker
- 32 Platenspeler (LP-speler)
- 33 Scheerapparaat
- 34 Uninterruptible Power Supply (UPS)
- 35 Playstation 3
- 36 Monitor
- 37 digitenne tv-ontvanger
- 38 Beamer
- 39 Vortexer
- 40 Xbox
- 41 Krultang
- 42 Microfoon
- 43 MP3-speler
- 44 Oven
- 45 Elektrisch rolluik
- 46 Stofzuiger
- 47 Camera
- 48 Haarstyler
- 49 Frituurpan
- 50 Bewegingsdetector
- 51 Diepvries
- 52 flip flap plant
- 53 broodrooster
- 54 Walkman
- 55 monitor
- 56 USB-muis
- 57 Computer
- 58 telefoonoplader
- 59 Tamagotchi
- 60 Nepbiertap
- 61 staafmixer
- 62 Haptic Arm
- 63 Dimmer
- 64 PSP
- 65 wafelijzer
- 66 warmtesensor
- 67 kookwekker
- 68 Zonnepaneel
- 69 Digitale buitentemperatuurmeter
- 70 Fohn
- 71 Stopcontact-schakelaar
- 72 Babyfoon
cd-speler
| domeinmodel | opmerkingen | |||||
|---|---|---|---|---|---|---|
|
||||||
Definition cdsp := cdsp_stroom ∧ cdsp_cd ∧ cdsp_aan → cdsp_lol ∧ cdsp_lor Als bij deze cd-speler op de stekker 230 V staan en een audio cd in de speler draait, en de aan/uit knop op 'aan' staat dan staan analoge geluidssignalen L, R op de line-uitgangen L, R en het digitale geluidssignaal op de optische uitgang. | ||||||
box links
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition boxl := boxl_in_l → mono_l Als bij deze box een versterkt mono-geluidssignaal L op de ingang staat is een mono-geluid L in de kamer te horen. | |
Synthesizer
| domeinmodel | opmerkingen | |||||
|---|---|---|---|---|---|---|
|
| |||||
Definition synth := synth_stroom ∧ synth_aan ∧ synth_bp → synth_lol ∧ synth_lor Als bij de synthesizer 12vdc op de voeding-ingang staat, de aan/uitschakelaar op aan staat en er wordt een toets op het klavier van de synthesizer ingedrukt dan staat er een geluidssignaal op de linker en rechter analoge uitgang van de synthesizer. | ||||||
box rechts
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition boxr := boxr_in_r -> mono_r Als bij deze box een versterkt mono-geluidssignaal R op de ingang staat is een mono-geluid R in de kamer te horen. | |
Subwoofer
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition subwoofer := subwoofer_in_sub → mono_sub Als bij deze subwoofer een versterkt mono-geluidssignaal Sub op de ingang staat is een mono-geluid Sub in de kamer te horen. | |
waterkoker
| domeinmodel | opmerkingen | |||||
|---|---|---|---|---|---|---|
|
||||||
Definition wk := (((wk_stroom ∧ wk_aan → wk_element) ∧ wk_water) → wk_kookt) Als bij deze waterkoker op de stekker 230 V staan en de aan/uit knop op 'aan' dan als wordt het verwarmingselement verwarmt en er water in de waterkoker zit dan wordt het water verwarmt tot het kookt | ||||||
Elektrisch Fornuis
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition ef := ef_stroom ∧ ((ef_lb_aan → ef_lb_warm) ∧ (ef_rb_aan → ef_rb_warm) ∧ (ef_ro_aan → ef_ro_warm) ∧ (ef_lo_aan → ef_lo_warm)) Een elektrisch fornuis met een viertal pitten. Als er stroom op het fornuis staat, en als de 'linksboven'-schakelaar ingeschakeld is dan wordt de 'linksboven'-pit warm, en als de 'rechtsboven'-schakelaar ingeschakeld is dan wordt de 'rechtsboven'-pit warm, en als de 'rechtsonder'-schakelaar ingeschakeld is dan wordt de 'rechtsonder'-pit warm, en als de 'linksonder'-schakelaar ingeschakeld is dan wordt de 'linksonder'-pit warm. | |
Magnetron
| domeinmodel | opmerkingen | |||||
|---|---|---|---|---|---|---|
|
| |||||
Definition mag := (mag_stroom ∧ mag_klok ∧ mag_dicht) → mag_aan Als bij deze magnetron op de stekker 230 V staat en de timer is ingesteld op een tijd en het deurtje is dicht, dan zend de magnetron microgolfen uit. | ||||||
Bureaulamp
| domeinmodel | opmerkingen | |||||
|---|---|---|---|---|---|---|
|
| |||||
Definition bl := bl_stroom ∧ bl_knop_aan ↔ bl_licht Als er op de stekker van de Bureaulamp 230v staat en de knop van de bureau lamp staat op aan, dan geeft de bureau lamp licht | ||||||
Koelkast
| domeinmodel | opmerkingen | |||||
|---|---|---|---|---|---|---|
|
| |||||
Definition klk := klk_stroom ∧ klk_aan ∧ klk_dicht → klk_koel Als er op de stekker van de koelkast 230V staat en de koelkast is ingeschakeld en de deur van de koelkast is dicht, koelt de koelkast. | ||||||
Boormachine
| domeinmodel | opmerkingen |
|---|---|
|
Het uitlopen na het loslaten van de machine is achterwegen gelaten. Dit is naar mijn weten niet met propositielogica te beschrijven. |
Definition bm_r := bm_sel ∧ bm_drr ∧ bm_ds → bm_dr Definition bm_l := bm_sel ∧¬ bm_drr ∧ bm_ds → bm_dr Als de stekker van de boormachine is ingeplugd op een correct werkende en daarvoor geschikt stroomnet en de draairichtingschakelaar staat rechtsom en de drukschakelaar is ingedrukt dan en slechts dan draait de boorkop rechtsom t.o.v. de machine. Als de stekker van de boormachine is ingeplugd op een correct werkende en daarvoor geschikt stroomnet en de draairichtingschakelaar staat niet rechtsom en de drukschakelaar is ingedrukt dan en slechts dan draait de boorkop linksom t.o.v. de machine. | |
Lichtsensor
| domeinmodel | opmerkingen |
|---|---|
|
Het is de bedoeling dat deze sensor stroom door laat als het donker is, het ¬-teken moet er blijven staan. |
Definition ls := ls_stroom_in ∧ ¬ls_licht ↔ ls_stroom_uit Er staat stroom op contact UIT dan en slechts dan als er stroom op contact IN staat en er niet genoeg licht valt op de sensor. | |
Strijkijzer
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition si := si_stroom ∧ si_knop_aan ∧ → si_ijzer_heet Als er op de stekker van het strijkijzer 230v staat en de knop van het strijkijzer staat op aan, dan wordt het warmte element heet | |
Tosti-ijzer
| domeinmodel | opmerkingen | |||||
|---|---|---|---|---|---|---|
ti_bakijzer_heet: het bakijzer wordt heet. Definition ti:= ti_stroom ∧ ti_knop ∧ ti_klep_dicht → ti_bakijzer_heet |
| |||||
|
{{{specificatie}}} Als er 230V op de stekker van het tosti-ijzer staat en de knop van het tosti-ijzer is ingedrukt en de klep van het tosti-ijzer is dicht dan wordt het bakijzer heet. | ||||||
Electrische tandenborstel
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition et := et_battvol ∧ et_aan → et_kop Als de batterij geladen is en spanning afgeeft en de aan/uit knop staat op aan dan maakt de borstelkop een draaibeweging. | |
draadloze telefoon
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition dt := et_bat ∧ dt_bereik ∧ dt_aan → dt_bellen als de telefoon aan is en de batterij opgeladen en je hebt bereik dan kun je bellen. | |
televisie
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition tv := tv_stroom ∧ tv_antennekabel ∧ tv_aan → tv_geeft_beeld Als er een spanning van 230 volt op de stekker van de televisie staat, de aan/uit-schakelaar is ingedrukt en een antennekabel signaal geeft aan de televisie dan geeft de televisie beeld in de vorm van optische signalen. | |
DVD-speler
| domeinmodel | opmerkingen | |||||
|---|---|---|---|---|---|---|
|
| |||||
Definition DVD-speler := DVD_stroom ∧ DVD_aan ∧ DVD_disc ∧ DVD_scart → DVD_avsign Als de DVD-speler is aangesloten op een 230v stopcontact, de DVD-speler aanstaat, er een DVD in de DVD-speler zit en de DVD-speler met een scart kabel is aangesloten op een tv dan wordt er een AV-signaal aan de tv doorgegeven | ||||||
TV (focus op AV voor bijv, een dvd speler)
| domeinmodel | opmerkingen |
|---|---|
|
Dit alles is met focus op het AV kanaal van de tv, andere functies van een tv zijn hier niet bij inbegrepen |
Definition TV := TV_stroom ∧ TV_aan ∧ TV_scart ∧ TV_AVkan → TV_AVbeeld ∧ TV_AVgeluid Als de TV is aangesloten op een 230v stopcontact, er een AV-signaal staat op de scart ingang van de TV, de TV aanstaat en de TV op het AV-kanaal staat dan is er beeld en geluid op het AV-kanaal van de TV | |
versterker
| domeinmodel | opmerkingen | |||||
|---|---|---|---|---|---|---|
|
Ik ga hier even uit van een versterker met 1 (stereo)invoer en 1 (stereo)uitvoer, hoewel dat er in de praktijk vaak meerdere zijn.
| |||||
Definition amp := (amp_stroom ∧ amp_on ∧ amp_inL → amp_outL) ∧ (amp_stroom ∧ amp_on ∧ amp_inR → amp_outR) Als de stekker van de versterker is aangesloten op netstroom van 220v, en de power-schakelaar staat aan, en er is een invoersignaal voor links en/of rechts, dan veeft de versterker uitvoer op de box(en) waar signaal voor is. | ||||||
Koffiezetapparaat
| domeinmodel | opmerkingen | |||||
|---|---|---|---|---|---|---|
|
| |||||
Definition kza := kza_stroom ∧ kza_water ∧ kza_filter ∧ kza_kan ∧ kza_aan → koffie Als de stekker van het koffiezetapparaat is aangesloten op de netstroom, en er zit water in het waterreservoir, en er zit een filter met gemalen koffie in de filterhouder, en de koffiekan staat onder de filterhouder, en het koffiezetapparaat staat aan, dan komt er koffie in de koffiekan. | ||||||
Rookmelder
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition rm := rm_stroom ∧ (rm_rook ∨ rm_testknop) ↔ rm_alarm Het alarm gaat af dan en slechts dan als 9 volt op de aansluitdraden van rookmelder staat, en er is rook in de sensor of de testknop is ingedrukt. | |
Rooksensor
| domeinmodel | opmerkingen |
|---|---|
|
rs_spanning
rs_ls_signaal
rs_alarm
|
|
|
Dan en slechts dan als de rooksensor spanning heeft en een signaal krijgt van zijn lichtsensor, slaat hij alarm Definition rs := rs_spanning /\ rs_ls_signaal <-> rs_alarm | |
Lichtsensor
| domeinmodel | opmerkingen |
|---|---|
|
ls_spanning
ls_lampje
ls_sensor
ls_signaal
|
|
|
Dan en slechts dan als de lichtsensor spanning heeft en zijn sensor geen licht, geeft hij een signaal Definition ls := ls_spanning /\ ls_lampje /\ ¬ls_sensor <-> ls_signaal | |
Stekkerdoos
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition sd := sd_stroom ∧ sd_aan → sd_stopcontact Als er op de stekker van de stekkerdoos 230V staat en de aan/uit knop op de stekkerdoos staat op aan dan staat er 230 V op de stopcontacten van de stekkerdoos. | |
Zwart/wit printer
| domeinmodel | opmerkingen |
|---|---|
|
Ik laat testpagina's buiten beschouwing. |
Definition zpr := zpr_stroom ∧ zpr_papier ∧ zpr_inkt ∧ zpr_opdracht ↔ zpr_print De printer print een printopdracht dan en slechts dan als er 230V op de stekker van de printer staat, er papier aanwezig is in de papierlader, er een niet-lege inktcartridge aanwezig is en de printer een printopdracht heeft ontvangen via de USB poort. | |
Thermostaat
| domeinmodel | opmerkingen |
|---|---|
|
Eventuele extra mogelijkheden zijn:
|
Definition Th := Th_stroom ∧ Th_hoog ∨ Th_laag ↔ ∃x € Th_toep [ Temp(x, 5~40)] Wanneer er 2 batterijen van 1,5v in de thermostaat zitten en de temperatuur gewijzigd wordt (omhoog danwel omlaag), is er een aangesloten toepassing (verwarming) waarbij de temperatuur veranderd tussen de 5 en 40 graden Celcius. | |
garagedeur bediening
| domeinmodel | opmerkingen |
|---|---|
T: verzamling van alle tijdstippen N: verzameling van de natuurlijke getallen |
De toegangsdeur hoeft niet per se open te zijn als de binnenknop bediend wordt, omdat hij na het openen weer gesloten kan worden, maar hij moet wel open geweest zijn, omdat iemand binnen moet zijn om de binnenknop te bedienen. |
Definition gdb := forall t: T, forall n,m:N, (SlInKBui t n /\ KBuiLi t n \/ TDeurOpen t-m /\ KBinLi t n) -> GDeurOmh t n forall t: T, forall n,m:N, (SlInKBui t n /\ KBuiRe t n \/ TDeurOpen t-m /\ KBinRe t n) -> GDeurOml t n forall t:T, forall n,m:N, ((KBinLi t n \/ KBinRe t n) /\ TDeurOpen t-m) /\ ((KBuiLi t n \/ KBuiRe t n) /\ SlInKBui t n) -> ~(GDeurOml t n \/ GDeurOmh t n) forall t:T, forall n,m,l:N, GDeurDicht t GDeurOmh t n /\ GDeurOml t+n m /\ GDeurOMh t+n+m l /\ n-m+l>10 --> GDeurOpen t+n+m+l forall t:T, forall n,m,l:N, GDeurOpen t GDeurOml t n /\ GDeurOmh t+n m /\ GDeurOMl t+n+m l /\ n-m+l>10 --> GDeurDicht t+n+m+l Als de buitenknop gedurende n seconden naar links is gedraaid terwijl de sleutel in de buitenknop zit,
of als de binnenknop gedurende n seconden naar links is gedraaid en de toegangsdeur op hetzelfde tijdstip of eerder open is (geweest),
gaat de garagedeur n seconden omhoog. | |
elektrische gitaar met solide body
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition gitaar := ((git_snaar → git_element) &or (git_voorwerp → git_element)) ∧ git_element_aan ∧ git_knop_aan → git_signaal_uit Als er door de trilling van een of meerdere snaren een elektrische stroom ontstaat in een of meerdere van de elementen of als er door (bijna)contact tussen een metalen voorwerp wat geen snaar is met een of meerdere van de elementen een elektrische stroom ontstaat in een of meerdere van de elementen en de schakelaar van een of meerdere van deze elementen waar een elektrische stroom ontstaat staat op 'aan' en de knop die de sterkte van het uitgaande signaal van de gitaar regelt staat niet op 0 gaat er een onversterkt signaal naar de jack van de gitaar. | |
Elektrische Tandenborstel
| domeinmodel | opmerkingen |
|---|---|
|
Alsjeblieft mijn opdracht niet weer verwijderen. Dit is de derde keer dat ik hem doe. |
Definition et := ( et_opgeladen ∧ et_aan ↔ et_timer ) ∧ ( et_opgeladen ∧ et_aan ↔ et_draait ) ∧ ( et_2min → ¬et_aan ) Als bij deze Elektrische Tandenborstel de batterij voldoende is opgeladen en de aan/uit-knop op 'aan' staat dan draait de borstel en loopt de interne timer. Als deze timer 2 minuten aangeeft dan stopt de borstel met draaien en stopt ook de timer. | |
mediacenter
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition mc := mc_stroom ∧ (mc_blu-ray ∨ mc_harddisk) ∧ mc_aan → mc_hdmi Als bij het mediacenter 230 V op de stekker staat en een cd/dvd/blu-ray disk draait in de blu-ray speler van het mediacenter of harddisk met films/muziek draait in het mediacenter, en de aan/uit knop staat aan dan staan het beeld en geluid signaal op de hdmi-uitgang. | |
Ventilator (2 standen)
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition mag := (vn_stroom ∧ vn_stand1 ∧ ¬vn_stand2 → vn_zacht) ∨ (vn_stroom ∧ vn_stand2 ∧ ¬vn_stand1 → vn_hard) Als de knop "stand 1" is ingedrukt en er stroom op de ventilator staat, draait de propeller van de ventilator zachtjes. Als de knop "stand 2" is ingedrukt en er stroom op de ventilator staat, draait de propeller van de ventilator hard. | |
Wekker
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition wek := wek_stroom ∧ wek_aan ∧ wek_tinst → (wek_tijd ↔ wek_alarm ∨ wek_snooze) Als de wekker is aangesloten op een spanningsbron van 230V (AC) of op de batterij en de wekker aan staat en er een tijd is ingesteld, dan en slechts dan zal wanneer de huidige tijd gelijk is aan de ingestelde tijd de wekker afgaan, of de snooze laten horen. | |
Platenspeler (LP-speler)
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition lps := lps_spanning ∧ lps_aan ∧ lps_plaat ∧ lps_elem → lps_phl ∧ lps_phr Als bij deze platenspeler 230V op de stekker staat en de afspeelknop staat op 'afspelen' en er draait een plaat en een element rust op de plaat, dan staan analoge geluidssignalen L,R op de phone-uitgangen L,R | |
Scheerapparaat
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition sa := ( sa_stroom \/ sa_accu ) /\ sa_aan → sa_mes Als er 230V op de stekker van het scheerapparaat staat of de accu is opgeladen met stroom en de aan/uit knop van het scheerapparaat staat op aan dan draaien de mesjes rond van het scheerapparaat. | |
Uninterruptible Power Supply (UPS)
| domeinmodel | opmerkingen |
|---|---|
|
De vraag is wat handiger/duidelijk is bij een accu: of axioma met een lege accu en inverse van het axioma in de definitie zetten, of axioma met (gedeeltelijk) opgeladen accu. De eerste lijkt mij makkelijker te definieren, vooral met korte propositienamen. Daarnaast een algemene opmerking: elk elektrisch apparaat kan op een UPS worden aangesloten i.p.v. direct op de netstroom, dus staat het wat raar als expliciet in de definitie van een apparaat staat dat deze op netstroom wordt aangesloten. |
Definition ups := ((ups_spanning_in \/ ¬ups_acculeeg) /\ ups_aan) ↔ ups_spanning_uit Als er 230V spanning op de ingang van de UPS staat of de accu niet leeg en de aan/uit knop van de UPS staat op 'aan' dan staat er 230V spanning op de uitgang van de UPS. | |
Playstation 3
| domeinmodel | opmerkingen |
|---|---|
|
PS3_stroom
PS3_aan
PS3_HDMI
|
|
definition Playstation 3:= PS3_stroom ∧ PS3_aan → PS3_HDMI Als er 230V stroom op de stekker van de Playstation 3 staat en als de aan/uit knop van de Playstation 3 op "aan" staat, dan staat er een digitaal signaal op de "HDMI-output" van de Playstation 3. | |
Monitor
| domeinmodel | opmerkingen |
|---|---|
|
M_stroom
M_aan
M_HDMI_in
M_HDMI_in_weergave
|
|
definition monitor:= M_stroom ∧ M_aan ∧ M_HDMI_in → M_HDMI_in_weergave Als er 230V stroom op de stekker van de monitor staat en als de aan/uit knop van de monitor op "aan" staat, en als er een digitaal signaal op de "HDMI-input" van de monitor staat, is er weergave van het digitale signaal wat binnenkomt op de "HDMI-input". | |
digitenne tv-ontvanger
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition ontv := ontv_stroom ^ ontv_aan ^ ontv_antenne ↔ ontv_beeld ^ ontv_geluid Als bij deze digitenne tv-ontvanger op de stekker 230 V staat en de aan/uit knop op 'aan' staat en de antenne goed geplaatst is dan is er een beeldsignaal op de scart-uitgang van de ontvanger. | |
Beamer
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition bea:= bea_stroom ∧ bea_aan ∧ bea_sign → bea_beeld Als de beamer is aangesloten op een 230 volt spanningsbron en de beamer staat aan en er staat een beeldsignaal op de input van de beamer, dan wordt het beeld gegenereerd/geprojecteerd. | |
Vortexer
| domeinmodel | opmerkingen |
|---|---|
|
Een vortexer wordt gebruikt om een reageerbuisje of Eppendorftube snel en krachtig te schudden. Meestal wordt de touch-mode gebruikt, en wordt het buisje of epje korte tijd op de rubberen bovenkant geduwd. |
Definition vor := vor_stroom ∧ (vor_aan V vor_touch ∧ vor_druk) → vor_tex Als bij deze vortexer op de stekker 230 V staat en de knop van de vortexer staat op 'aan', of de knop staat op 'touch' en er wordt druk uitgeoefend op de kop van de vortexer, dan vibreert de vortexter. | |
Xbox
| domeinmodel | opmerkingen | |||||
|---|---|---|---|---|---|---|
|
| |||||
Definition Xbox := (xbox_aan ∧ xbox_stroom xbox_tv) ⇔ xbox_beeld Dan en slechts dan als de Xbox is aangesloten op 230 volt en als de Xbox is aangesloten op een tv en als de aan-knop is ingedrukt,geeft de Xbox beeld. | ||||||
Krultang
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition klt := (klt_stroom ∧ klt_aan) → klt_warm Als bij deze krultang 230 V op de stekker staat en hij staat aan dan word de krultang verwarmd. | |
Microfoon
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition mic := mic_aan ∧ mic_geluid → mic_lo Als deze microfoon geluid opvangt en de aan/uit knop op 'aan' staat dan staat analoog geluidssignaal op de uitgang van de microfoon | |
MP3-speler
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition mp3 := (mp3_batterij /\ mp3_start -> mp3_aan) /\ (mp3_aan /\ mp3_play /\ mp3_geheugen -> mp3_speelt) Als er een opgeladen batterij in de mp3-speler zit en de play-knop wordt langer dan een seconde ingedrukt dan gaat de mp3-speler aan. En als de mp3-speler aan is en de play0knop wordt minder dan een seconde ingedrukt dan speelt hij een liedje af.(Als er liedjes op staan). | |
Oven
| domeinmodel | opmerkingen |
|---|---|
|
Gemodelleerd naar mijn eigen oven. |
Definition oven := (((oven_stroom ↔ oven_aan) ∧ (oven_tdgr → oven_wkr) ∧ oven_tmpkl) ↔ oven_lmnt → oven_verw) De oven verwarmd als het verwarmingselement aanstaat van de oven. Het verwarmingselement staat aan dan en slechts dan als de huidige temperatuur in de oven kleiner is dan de ingestelde temperatuur te samen met de wekker aan staat én de oven aanstaat. De oven staat aan dan en slechts dan als er 230 volt wisselspanning op de stekker van de oven staat (aannemende dat de stekker van de oven verbonden is met de oven). De wekker staat aan als de tijd op de wekker groter is dan 0; | |
Elektrisch rolluik
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition rol := rol_spanning ∧ rol_ko ∧ ~rol_open → rol_omh Als de stroomdraden van de motor zijn verbonden met een spanning van 230V, en de bedieningsknop staat in de stand voor omhoog, en het rolluik is nog niet helemaal omhoog, dan beweegt het rolluik omhoog. | |
Stofzuiger
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition sz := (sz_stroom ∧ sz_aan) ↔ sz_motor De motor van de stofzuiger staat aan dan en slechts dan als de stofzuiger stroom heeft en aan staat. | |
Camera
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition Camera: ((camera_stroom /\ werk_geheugen_vrij /\ card_geheugen_vrij /\ (afstandsbediening \/ sluiter)) <-> foto) Er wordt een foto gemaakt dan en slechts dan als een camera genoeg stroom heeft en voldoende geheugen vrij heeft in de memory-card en in het werkgeheugen en de sluiterknop is ingedrukt of de afstandsbediening een signaal uitzendt naar de camera om een foto te maken. | |
Haarstyler
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition stl := (stl_stroom v stl_accu) ∧ stl_aan -> stl_borstel ∧ stl_warm; Als er 230 V op de stekker van de styler staat of de accu is opgeladen met stroom en de styler staat aan dan draait de borstel rond en komt er warme lucht uit de borstel. | |
Frituurpan
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition fp := (fp_stroom ∧ fp_aan → fp_verwElem) ∧ fp_olie ∧ fp_snacks → fp_gefrituurd Als er stroom op de stekker staat en de frituurpan staat aan, dan wordt het element verwarmd. Als dit geldt, en er zit olie in de pan, en er zitten snacks in de pan, dan worden de snacks gefrituurd. | |
Bewegingsdetector
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition bd:= bd_stroom_in ∧ bd_aan ∧ bd_beweging → bd_stroom_uit Als er batterijen in de bewegingsdetector zitten, en de bewegingsdetector is ingeschakeld en er is beweging in het gezichtsveld van de bewegingsdetector, dan staat er spanning op de uit-poort (naar bijvoorbeeld een buitenlamp). | |
Diepvries
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition boxl := (dpvr_stroom ∧ dpvr_aan ∧ dpvr_dicht) → dpvr_vriest Als er stroom staat op de koelkast, en de koelkast staat aan met de deur dicht, dan vriest de diepvries. | |
flip flap plant
| domeinmodel | opmerkingen | |||||
|---|---|---|---|---|---|---|
|
Een flipflap plant is natuurlijk een plastic plantje wat gaat bewegen wanneer er licht op valt. Voor de duidelijkheid is een foto bijgevoegd:
| |||||
Definition flipflap := (ff_licht^ff_aangeraakt) <-> ff_beweeg Als er licht of de flipflap plant schijnt gaat hij bewegen | ||||||
broodrooster
| domeinmodel | opmerkingen |
|---|---|
|
{{{opmerkingen}}} |
Definition broodrooster := brdrstr_stroom ∧ brdrstr_broodInRooster ∧ brdrstr_aan → brdrstr_brood_wordt_geroostert Als de stekker in het stopcontact zit, er op de aanknop is gedrukt en er brood in zit, zal dat brood geroostert worden. | |
Walkman
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition Walkman := (wm_batt ∧ wm_cass ∧ wm_play) ↔ (wm_aam ∧ wm_mus) Als er een batterij en cassette in de walkman zitten, en als de playknop ingedrukt is dan gaat de cassette draaien en komt er geluid uit | |
monitor
| domeinmodel | opmerkingen |
|---|---|
|
{{{opmerkingen}}} |
Definition monitor := mntr_stroom ∧ mntr_aangesloten ∧ mntr_aan: de aan-uit knop ∧ mntr_krijgt_beeld ->mntr_er_komt_een_beeld_op_de_monitor Als er stroom op de steker van de monitor zit en die zit aangesloten op het scherm en de monitor staat op aan en krijgt een beeld binnen dat compatible is dan komt er een beeld weer gegeven op de monitor . | |
USB-muis
| domeinmodel | opmerkingen |
|---|---|
|
{{{opmerkingen}}} |
Definition muis := muis_USB → (muis_Lklik ↔ muis_Ls) ∧ (muis_Rklik ↔ muis_Rs) Als de muis in een werkende USB-poort is gestoken, dan geldt dat als het indrukken van de linker- of rechtermuisknop leidt tot het bijbehorende signaal aan de USB-poort, deze signalen worden niet verstuurd als er niet op de muisknop gedrukt wordt. | |
Computer
| domeinmodel | opmerkingen |
|---|---|
|
{{{opmerkingen}}} |
Definition pc := pc_stroom ↔ (pc_USB ∧ (pc_aan ↔ pc_HDMI)) Als de pc stroomtoevoer heeft, werken de USB-poorten, en geldt dat als de pc aan staat, er een beeldsignaal naar de HDMI-uitvoer gestuurd wordt. | |
telefoonoplader
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition to := to_spanning ∧ to_aangesloten → to_opladen Als bij deze oplader op de stekker 230V staat en er een telefoon is aangesloten op de uitgang van de oplader dan staat er 5V op de uitgang | |
Tamagotchi
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition tmg := (tmg_honger ∨ tmg_toilet ∨ tmg_spelen) → tmg_irritant Een Tamagotchi is altijd aan, maar daarbinnen is hij irritant dan maar niet eens slechts dan als hij om aandacht vraagt. | |
Nepbiertap
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition nbt := nbt_stroom ∧ nbt_aan --> nbt_pomp Als er 230 V op de stekker van de nepbiertap staat en de aan/uit knop van de nepbiertap staat op aan dan pompt de biertap vloeistof rond. | |
staafmixer
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition stfmxr := (stfmxr_stroom ∧ stfmxr_knop → stfmxr_motor) ∧ (stfmxr_motor → stfmxr_mesjes) Als het zo is dat als bij deze staafmixer op de stekker 230 V staat en de knop is ingedrukt dan de motor beweegt, dan draaien de mesjes. | |
Haptic Arm
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition HapticArm := electricity -> (
(control <-> torque)
/\
(touch <-> feedback)
).
if the haptic arm is powered, then... when it is controlled it will exert torque and when it touches something it will provide feedback | |
Dimmer
| domeinmodel | opmerkingen |
|---|---|
|
Omdat het moeilijk is om een continue schaal te vertalen in propositie logica maak ik gebruik twee standen; "veel dimmen" en "weinig dimmen". |
Definition dmr := (dmr_stroom_in /\ dmr_draaiknop_hoog -> dmr_stroom_uit_hoog) \/ (dmr_stroom_in /\ dmr_draaiknop_laag -> dmr_stroom_uit_laag) Als er stroom op de dimmer staat en de draaiknop staat op stand 'hoog', dan komt er stroom op een hoog wattage uit. Als er stroom op de dimmer staat en de draaiknop staat op stand 'laag', dan komt er stroom op een laag wattage uit. | |
PSP
| domeinmodel | opmerkingen |
|---|---|
|
{{{opmerkingen}}} |
Definition PSP := (psp_oplader_in \/ psp_batterij_niet_leeg) ∧ psp_aan → psp_beeld Als de batterij van de psp niet leeg is, of de oplader van de psp is ingestoken en de psp staat aan, dan geeft het beeldscherm van de psp een signaal en kan er op gespeeld worden. | |
wafelijzer
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition wa : wa_stroom ∧ wa_knop → wa_heet Als de knop is ingedrukt en zit strom op de wafelijzer dan wordt die heet | |
warmtesensor
| domeinmodel | opmerkingen |
|---|---|
|
Er staat een stroom op ws_stroom_uit dan en slechts dan als er stroom op ws_stroom_in staat en de temperatuur die ws_temp meet kleiner of gelijk 150 graden Celsius is. |
Definition ws := ws_stroom_in ∧ (ws_temp <= 150) ↔ ws_stroom_uit
| |
kookwekker
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition kookwekker:= kw_batterijvol ∧ kw_is_ingesteld ∧ kw_staat_op_nul -> kw_rinkelt Als de batterij is geladen en spanning af geeft en de kookwekker aanstaat en de kookwekker is ingesteld en staat nu op nul, dan rinkelt hij. | |
Zonnepaneel
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition Zonnepaneel := (L_zonlicht \/ L_maanlicht) /\ L_aan --> L_stroom Als er voldoende zonlicht of maanlicht op het zonnepaneel valt en de aan/uit schakelaar van het zonnepaneel staat op 'aan' dan wekt het zonnepaneel energie op. | |
Digitale buitentemperatuurmeter
| domeinmodel | opmerkingen |
|---|---|
|
|
Def buitentemperatuurmeter := btemp_sensor ∧ btemp_ontvanger → btemp_verwerking ∧ btemp_display Als de sensor een signaal uitzend en de ontvanger ontvangt het singaal dan wordt het signaal verwerkt en toont de display het resultaat | |
Fohn
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition fhn := (fhn_stroom /\ fhn_aan -> fhn_gloei /\ fhn_vent) -> fhn_fohnt Als er 230 V op de stekker van de fohn staat en de aan/uitschakelijk aan staat word het gloei element warm, gaat de ventilator draaien en blaast de fohn warmelucht. | |
Stopcontact-schakelaar
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition stc := stc_stroom /\ stc_aan -> stc_stroom_uit /\ stc_lamp Als er 230 V op de stekker van stopcontact-schakelaar staat en het laat stroom door staat er op het stopcontact van de stopcontact-schakelaar 230 V. | |
Babyfoon
| domeinmodel | opmerkingen |
|---|---|
|
|
Definition babyfoon := (bf_ontvanger_aan /\ bf_zender_aan) /\ bf_huil -> bf_zend /\ bf_speel Als de zender en de ontvanger aan staan, en een baby begint te huilen bij de zender in de buurt, dan zal de zender dat doorsturen en begint de ontvanger het gejank te laten horen | |
